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 7c488f524..cc9d98f6f 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -142,7 +142,7 @@ let rec add_prods_sign env sigma t = let compute_first_inversion_scheme env sigma ind sort dep_option = let indf,realargs = dest_ind_type ind in - let allvars = ids_of_context env in + let allvars = vars_of_env env in let p = next_ident_away (Id.of_string "P") allvars in let pty,goal = if dep_option then @@ -214,7 +214,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = else Context.Named.add d sign) invEnv ~init:Context.Named.empty end in - let avoid = ref [] in + let avoid = ref Id.Set.empty in let { sigma=sigma } = Proof.V82.subgoals pf in let sigma = Evd.nf_constraints sigma in let rec fill_holes c = @@ -222,7 +222,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = | Evar (e,args) -> let h = next_ident_away (Id.of_string "H") !avoid in let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in - avoid := h::!avoid; + avoid := Id.Set.add h !avoid; ownSign := Context.Named.add (LocalAssum (h,ty)) !ownSign; applist (mkVar h, inst) | _ -> EConstr.map sigma fill_holes c |