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. --- engine/proofview.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/proofview.ml') diff --git a/engine/proofview.ml b/engine/proofview.ml index 9adf94744..9e5e9c7da 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -984,7 +984,7 @@ module Goal = struct type ('a, 'r) t = { env : Environ.env; sigma : Evd.evar_map; - concl : Term.constr ; + concl : EConstr.constr ; self : Evar.t ; (* for compatibility with old-style definitions *) } @@ -1005,7 +1005,7 @@ module Goal = struct let gmake_with info env sigma goal = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; sigma = sigma ; - concl = Evd.evar_concl info ; + concl = EConstr.of_constr (Evd.evar_concl info); self = goal } let nf_gmake env sigma goal = -- cgit v1.2.3