Definining EConstr-based contexts.

This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.

1 files changed, 8 insertions, 7 deletions

diff --git a/engine/proofview.mli b/engine/proofview.mli
index 9f10e874a..025e3de20 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -14,6 +14,7 @@
 
 open Util
 open Term
+open EConstr
 
 (** Main state of tactics *)
 type proofview
@@ -43,7 +44,7 @@ val compact : entry -> proofview -> entry * proofview
     empty [evar_map] (indeed a proof can be triggered by an incomplete
     pretyping), [init] takes an additional argument to represent the
     initial [evar_map]. *)
-val init : Evd.evar_map -> (Environ.env * EConstr.types) list -> entry * proofview
+val init : Evd.evar_map -> (Environ.env * types) list -> entry * proofview
 
 (** A [telescope] is a list of environment and conclusion like in
     {!init}, except that each element may depend on the previous
@@ -52,7 +53,7 @@ val init : Evd.evar_map -> (Environ.env * EConstr.types) list -> entry * proofvi
     [evar_map] is threaded in state passing style. *)
 type telescope =
   | TNil of Evd.evar_map
-  | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
+  | TCons of Environ.env * Evd.evar_map * types * (Evd.evar_map -> constr -> telescope)
 
 (** Like {!init}, but goals are allowed to be dependent on one
     another. Dependencies between goals is represented with the type
@@ -69,8 +70,8 @@ val finished : proofview -> bool
 (** Returns the current [evar] state. *)
 val return : proofview -> Evd.evar_map
 
-val partial_proof : entry -> proofview -> EConstr.constr list
-val initial_goals : entry -> (EConstr.constr * EConstr.types) list
+val partial_proof : entry -> proofview -> constr list
+val initial_goals : entry -> (constr * types) list
 
 
 
@@ -484,15 +485,15 @@ 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 -> EConstr.constr
-  val hyps : ([ `NF ], 'r) t -> Context.Named.t
+  val concl : ([ `NF ], 'r) t -> constr
+  val hyps : ([ `NF ], 'r) t -> named_context
   val env : ('a, 'r) t -> Environ.env
   val sigma : ('a, 'r) t -> 'r Sigma.t
   val extra : ('a, 'r) t -> Evd.Store.t
 
   (** Returns the goal's conclusion even if the goal is not
       normalised. *)
-  val raw_concl : ('a, 'r) t -> EConstr.constr
+  val raw_concl : ('a, 'r) t -> constr
 
   type ('a, 'b) enter =
     { enter : 'r. ('a, 'r) t -> 'b }