diff options
| author | Pierre-Marie Pédrot | 2018-04-14 13:46:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-04-14 13:46:05 +0200 |
| commit | 2384fcb98640dbd9aeee4e8e43965d499e594815 (patch) | |
| tree | c7aaa89a76405ab8695d26590d76a971a170c850 /plugins/ssr/ssrequality.ml | |
| parent | 4f6681a4835758a27aaade3c18c21a5fe6d283c5 (diff) | |
| parent | e158df83522215b7699879c38906471598217866 (diff) | |
Merge PR #7136: Evar maps contain econstrs.
Diffstat (limited to 'plugins/ssr/ssrequality.ml')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 2f0433b642..7748ba2b0c 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -359,7 +359,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let evs = Evar.Set.elements (Evarutil.undefined_evars_of_term sigma t) in let open_evs = List.filter (fun k -> Sorts.InProp <> Retyping.get_sort_family_of - env sigma (EConstr.of_constr (Evd.evar_concl (Evd.find sigma k)))) + env sigma (Evd.evar_concl (Evd.find sigma k))) evs in if open_evs <> [] then Some name else None) (List.combine (Array.to_list args) names) @@ -478,10 +478,10 @@ let rwprocess_rule dir rule gl = | _ -> let ra = Array.append a [|r|] in function 1 -> let sigma, pi1 = Evd.fresh_global env sigma coq_prod.Coqlib.proj1 in - EConstr.mkApp (EConstr.of_constr pi1, ra), sigma + EConstr.mkApp (pi1, ra), sigma | _ -> let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in - EConstr.mkApp (EConstr.of_constr pi2, ra), sigma in + EConstr.mkApp (pi2, ra), sigma in if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ())) then let s, sigma = sr sigma 2 in loop (converse_dir d) sigma s a.(1) rs 0 |