diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
| commit | 1ef7f1c0c6897535a86daa77799714e25638f5e9 (patch) | |
| tree | 5bcca733632ecc84d2c6b1ee48cb2e557a7adba5 /plugins/ssr/ssrelim.ml | |
| parent | 3a2fac7bcee36fd9dcb4f39a615c8ac0349abcc9 (diff) | |
| parent | 9ebf44d84754adc5b64fcf612c6816c02c80462d (diff) | |
Updated version 8.9.0 from 'upstream/8.9.0'
with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63
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 |