exception in remove tactic

[bodeveix]

An exception is raised by the remove tactic from function codom_binder when the list of hypotheses contains a defined variable.

The following modified code (libTerm.ml) seems to solve the problem:

let rec codom_binder : int -> term -> binder = fun n t ->
match unfold t with
| Prod(_,b) ->
if n <= 0 then b else codom_binder (n-1) (subst b mk_Kind)
| LLet(a,t,u) ->
if n <= 0 then u else codom_binder (n-1) (subst u a)
| _ -> assert false