From e09f3b44bb381854b647a6d9debdeddbfc49177e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 22:16:08 +0100 Subject: Proofview.Goal primitive now return EConstrs. --- plugins/ssrmatching/ssrmatching.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ssrmatching') diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index aa91494eb..d34c9325e 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1078,7 +1078,7 @@ END let thin id sigma goal = let ids = Id.Set.singleton id in let env = Goal.V82.env sigma goal in - let cl = EConstr.Unsafe.to_constr (Goal.V82.concl sigma goal) in + let cl = Goal.V82.concl sigma goal in let evdref = ref (Evd.clear_metas sigma) in let ans = try Some (Evarutil.clear_hyps_in_evi env evdref (Environ.named_context_val env) cl ids) -- cgit v1.2.3