Proofview.Goal primitive now return EConstrs.

4 files changed, 6 insertions, 5 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 204997445..73286f2c4 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -611,6 +611,7 @@ let clear_hyps_in_evi_main env evdref hyps terms ids =
   (nhyps,terms)
 
 let clear_hyps_in_evi env evdref hyps concl ids =
+  let concl = EConstr.Unsafe.to_constr concl in
   match clear_hyps_in_evi_main env evdref hyps [concl] ids with
   | (nhyps,[nconcl]) -> (nhyps,nconcl)
   | _ -> assert false
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index cf36f5953..5882f02b9 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -199,7 +199,7 @@ exception ClearDependencyError of Id.t * clear_dependency_error
     used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*)
 val cleared : bool Store.field
 
-val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
+val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> EConstr.types ->
   Id.Set.t -> named_context_val * types
 
 val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types ->
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 =
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 725445251..2350592a2 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -484,7 +484,7 @@ module Goal : sig
       respectively the conclusion of [gl], the hypotheses of [gl], the
       environment of [gl] (i.e. the global environment and the
       hypotheses) and the current evar map. *)
-  val concl : ([ `NF ], 'r) t -> Term.constr
+  val concl : ([ `NF ], 'r) t -> EConstr.constr
   val hyps : ([ `NF ], 'r) t -> Context.Named.t
   val env : ('a, 'r) t -> Environ.env
   val sigma : ('a, 'r) t -> 'r Sigma.t
@@ -492,7 +492,7 @@ module Goal : sig
 
   (** Returns the goal's conclusion even if the goal is not
       normalised. *)
-  val raw_concl : ('a, 'r) t -> Term.constr
+  val raw_concl : ('a, 'r) t -> EConstr.constr
 
   type ('a, 'b) enter =
     { enter : 'r. ('a, 'r) t -> 'b }