diff options
Diffstat (limited to 'tactics/leminv.ml')
| -rw-r--r-- | tactics/leminv.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 46f1f7c8d..85910355e 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -116,7 +116,7 @@ let max_prefix_sign lid sign = | id::l -> snd (max_rec (id, sign_prefix id sign) l) *) let rec add_prods_sign env sigma t = - match kind_of_term (whd_all env sigma t) with + match kind_of_term (whd_all env sigma (EConstr.of_constr t)) with | Prod (na,c1,b) -> let id = id_of_name_using_hdchar env t na in let b'= subst1 (mkVar id) b in @@ -169,7 +169,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let goal = mkArrow i (applist(mkVar p, List.rev revargs)) in (pty,goal) in - let npty = nf_all env sigma pty in + let npty = nf_all env sigma (EConstr.of_constr pty) in let extenv = push_named (LocalAssum (p,npty)) env in extenv, goal @@ -183,7 +183,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let inversion_scheme env sigma t sort dep_option inv_op = let (env,i) = add_prods_sign env sigma t in let ind = - try find_rectype env sigma i + try find_rectype env sigma (EConstr.of_constr i) with Not_found -> user_err ~hdr:"inversion_scheme" (no_inductive_inconstr env sigma i) in |