diff options
Diffstat (limited to 'plugins/ssr/ssrelim.ml')
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 40af5187..602fcfca 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -14,9 +14,10 @@ open Util open Names open Printer open Term +open Constr open Termops open Globnames -open Misctypes +open Tactypes open Tacmach open Ssrmatching_plugin @@ -358,7 +359,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let ev = List.fold_left Evar.Set.union Evar.Set.empty patterns_ev in let ty_ev = Evar.Set.fold (fun i e -> let ex = i in - let i_ty = EConstr.of_constr (Evd.evar_concl (Evd.find (project gl) ex)) in + let i_ty = Evd.evar_concl (Evd.find (project gl) ex) in Evar.Set.union e (evars_of_term i_ty)) ev Evar.Set.empty in let inter = Evar.Set.inter ev ty_ev in @@ -420,7 +421,7 @@ let injectl2rtac sigma c = match EConstr.kind sigma c with let is_injection_case c gl = let gl, cty = pfe_type_of gl c in let (mind,_), _ = pf_reduce_to_quantified_ind gl cty in - eq_gr (IndRef mind) (Coqlib.build_coq_eq ()) + GlobRef.equal (IndRef mind) (Coqlib.build_coq_eq ()) let perform_injection c gl = let gl, cty = pfe_type_of gl c in |