aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-05-16 11:11:51 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-05-16 11:11:51 +0200
commitc122e1827aae252716da56ab46eeed4046c4aefc (patch)
treede16215c11580a284b9c539c93e381efdcecf6f7 /plugins/ssr
parent768883a6b7002bcdc589b43c199b2c0b1d2c23b5 (diff)
[ssr] fix after to_constr ~abort_on_undefined_evars was added
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrequality.ml5
-rw-r--r--plugins/ssr/ssrview.ml2
2 files changed, 5 insertions, 2 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 7d7655d29..eadc6d218 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -287,7 +287,10 @@ let foldtac occ rdx ft gl =
(fun env c _ h -> try find_T env c h ~k:(fun env t _ _ -> t) with NoMatch ->c),
(fun () -> try end_T () with NoMatch -> fake_pmatcher_end ())
| _ ->
- (fun env c _ h -> try let sigma = unify_HO env sigma (EConstr.of_constr c) (EConstr.of_constr t) in EConstr.to_constr sigma (EConstr.of_constr t)
+ (fun env c _ h ->
+ try
+ let sigma = unify_HO env sigma (EConstr.of_constr c) (EConstr.of_constr t) in
+ EConstr.to_constr ~abort_on_undefined_evars:false sigma (EConstr.of_constr t)
with _ -> errorstrm Pp.(str "fold pattern " ++ pr_constr_pat t ++ spc ()
++ str "does not match redex " ++ pr_constr_pat c)),
fake_pmatcher_end in
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index fc50b24a6..29a936381 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -260,7 +260,7 @@ Goal.enter_one ~__LOC__ begin fun g ->
let p = Reductionops.nf_evar sigma p in
let get_body = function Evd.Evar_defined x -> x | _ -> assert false in
let evars_of_econstr sigma t =
- Evd.evars_of_term (EConstr.to_constr sigma (EConstr.of_constr t)) in
+ Evarutil.undefined_evars_of_term sigma (EConstr.of_constr t) in
let rigid_of s =
List.fold_left (fun l k ->
if Evd.is_defined sigma k then