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, 50 insertions, 49 deletions

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 67de18abc..2da4f8043 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -10,6 +10,7 @@ open Names
 open Term
 open Evd
 open Environ
+open EConstr
 
 (** This module provides useful higher-level functions for evar manipulation. *)
 
@@ -17,51 +18,51 @@ open Environ
 
 (** [new_meta] is a generator of unique meta variables *)
 val new_meta : unit -> metavariable
-val mk_new_meta : unit -> EConstr.constr
+val mk_new_meta : unit -> constr
 
 (** {6 Creating a fresh evar given their type and context} *)
 val new_evar :
   env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?candidates:EConstr.constr list -> ?store:Store.t ->
+  ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> EConstr.types -> (EConstr.constr, 'r) Sigma.sigma
+  ?principal:bool -> types -> (constr, 'r) Sigma.sigma
 
 val new_pure_evar :
   named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?candidates:EConstr.constr list -> ?store:Store.t ->
+  ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> EConstr.types -> (evar, 'r) Sigma.sigma
+  ?principal:bool -> types -> (evar, 'r) Sigma.sigma
 
 val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma
 
 (** the same with side-effects *)
 val e_new_evar :
   env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?candidates:EConstr.constr list -> ?store:Store.t ->
+  ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> EConstr.types -> EConstr.constr
+  ?principal:bool -> types -> constr
 
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
 val new_type_evar :
   env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid ->
-  (EConstr.constr * sorts, 'r) Sigma.sigma
+  (constr * sorts, 'r) Sigma.sigma
 
 val e_new_type_evar : env -> evar_map ref ->
   ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> EConstr.constr * sorts
+  ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts
 
-val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (EConstr.constr, 'r) Sigma.sigma
-val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> EConstr.constr
+val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
+val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
 
 val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t ->
-  EConstr.constr list option -> (existential_key, 'r) Sigma.sigma
+  constr list option -> (existential_key, 'r) Sigma.sigma
 
 (** Polymorphic constants *)
 
-val new_global : 'r Sigma.t -> Globnames.global_reference -> (EConstr.constr, 'r) Sigma.sigma
-val e_new_global : evar_map ref -> Globnames.global_reference -> EConstr.constr
+val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma
+val e_new_global : evar_map ref -> Globnames.global_reference -> constr
 
 (** Create a fresh evar in a context different from its definition context:
    [new_evar_instance sign evd ty inst] creates a new evar of context
@@ -70,15 +71,15 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> EConstr.constr
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
- named_context_val -> 'r Sigma.t -> EConstr.types -> 
-  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:EConstr.constr list ->
+ named_context_val -> 'r Sigma.t -> types -> 
+  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list ->
   ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool ->
-  EConstr.constr list -> (EConstr.constr, 'r) Sigma.sigma
+  constr list -> (constr, 'r) Sigma.sigma
 
 val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list
 
-val safe_evar_value : evar_map -> existential -> constr option
+val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option
 
 (** {6 Evars/Metas switching...} *)
 
@@ -88,15 +89,15 @@ val non_instantiated : evar_map -> evar_info Evar.Map.t
 
 (** [head_evar c] returns the head evar of [c] if any *)
 exception NoHeadEvar
-val head_evar : evar_map -> EConstr.constr -> existential_key (** may raise NoHeadEvar *)
+val head_evar : evar_map -> constr -> existential_key (** may raise NoHeadEvar *)
 
 (* Expand head evar if any *)
-val whd_head_evar :  evar_map -> EConstr.constr -> EConstr.constr
+val whd_head_evar :  evar_map -> constr -> constr
 
 (* An over-approximation of [has_undefined (nf_evars evd c)] *)
-val has_undefined_evars : evar_map -> EConstr.constr -> bool
+val has_undefined_evars : evar_map -> constr -> bool
 
-val is_ground_term :  evar_map -> EConstr.constr -> bool
+val is_ground_term :  evar_map -> constr -> bool
 val is_ground_env  :  evar_map -> env -> bool
 
 (** [gather_dependent_evars evm seeds] classifies the evars in [evm]
@@ -121,14 +122,14 @@ val advance : evar_map -> evar -> evar option
     This is roughly a combination of the previous functions and
     [nf_evar]. *)
 
-val undefined_evars_of_term : evar_map -> EConstr.constr -> Evar.Set.t
+val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t
 val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t
 val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t
 
 (** [occur_evar_upto sigma k c] returns [true] if [k] appears in
     [c]. It looks up recursively in [sigma] for the value of existential
     variables. *)
-val occur_evar_upto : evar_map -> Evar.t -> EConstr.t -> bool
+val occur_evar_upto : evar_map -> Evar.t -> constr -> bool
 
 (** {6 Value/Type constraints} *)
 
@@ -139,18 +140,18 @@ val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma
 (** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains
     uninstantiated; [nf_evar] leaves uninstantiated evars as is *)
 
-val whd_evar :  evar_map -> EConstr.constr -> EConstr.constr
-val nf_evar :  evar_map -> EConstr.constr -> EConstr.constr
-val j_nf_evar :  evar_map -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment
+val whd_evar :  evar_map -> constr -> constr
+val nf_evar :  evar_map -> constr -> constr
+val j_nf_evar :  evar_map -> unsafe_judgment -> unsafe_judgment
 val jl_nf_evar :
-   evar_map -> EConstr.unsafe_judgment list -> EConstr.unsafe_judgment list
+   evar_map -> unsafe_judgment list -> unsafe_judgment list
 val jv_nf_evar :
-   evar_map -> EConstr.unsafe_judgment array -> EConstr.unsafe_judgment array
+   evar_map -> unsafe_judgment array -> unsafe_judgment array
 val tj_nf_evar :
-   evar_map -> EConstr.unsafe_type_judgment -> EConstr.unsafe_type_judgment
+   evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
 val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t
-val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t
+val nf_rel_context_evar : evar_map -> rel_context -> rel_context
 val nf_env_evar : evar_map -> env -> env
 
 val nf_evar_info : evar_map -> evar_info -> evar_info
@@ -159,39 +160,39 @@ val nf_evar_map_undefined : evar_map -> evar_map
 
 (** Presenting terms without solved evars *)
 
-val nf_evars_universes : evar_map -> constr -> constr
+val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr
 
-val nf_evars_and_universes : evar_map -> evar_map * (constr -> constr)
-val e_nf_evars_and_universes : evar_map ref -> (constr -> constr) * Universes.universe_opt_subst
+val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)
+val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst
 
 (** Normalize the evar map w.r.t. universes, after simplification of constraints.
     Return the substitution function for constrs as well. *)
-val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr)
+val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)
 
 (** Replacing all evars, possibly raising [Uninstantiated_evar] *)
 exception Uninstantiated_evar of existential_key
-val flush_and_check_evars :  evar_map -> EConstr.constr -> constr
+val flush_and_check_evars :  evar_map -> constr -> Constr.constr
 
 (** {6 Term manipulation up to instantiation} *)
 
 (** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t]
     as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the
     value of [e] in [sigma] is (recursively) used. *)
-val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term
+val kind_of_term_upto : evar_map -> Constr.constr -> (Constr.constr,Constr.types) kind_of_term
 
 (** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
     [u] up to existential variable instantiation and equalisable
     universes. The term [t] is interpreted in [sigma1] while [u] is
     interpreted in [sigma2]. The universe constraints in [sigma2] are
     assumed to be an extention of those in [sigma1]. *)
-val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
+val eq_constr_univs_test : evar_map -> evar_map -> Constr.constr -> Constr.constr -> bool
 
 (** {6 Removing hyps in evars'context}
 raise OccurHypInSimpleClause if the removal breaks dependencies *)
 
 type clear_dependency_error =
 | OccurHypInSimpleClause of Id.t option
-| EvarTypingBreak of existential
+| EvarTypingBreak of Constr.existential
 
 exception ClearDependencyError of Id.t * clear_dependency_error
 
@@ -199,7 +200,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 -> EConstr.types ->
+val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
   Id.Set.t -> named_context_val * types
 
 val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types ->
@@ -208,19 +209,19 @@ val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> ty
 type csubst
 
 val empty_csubst : csubst
-val csubst_subst : csubst -> EConstr.t -> EConstr.t
+val csubst_subst : csubst -> constr -> constr
 
 type ext_named_context =
-  csubst * (Id.t * EConstr.constr) list *
-  Id.Set.t * Context.Named.t
+  csubst * (Id.t * constr) list *
+  Id.Set.t * named_context
 
 val push_rel_decl_to_named_context :
-  Context.Rel.Declaration.t -> ext_named_context -> ext_named_context
+  rel_declaration -> ext_named_context -> ext_named_context
 
-val push_rel_context_to_named_context : Environ.env -> EConstr.types ->
-  named_context_val * EConstr.types * EConstr.constr list * csubst * (identifier*EConstr.constr) list
+val push_rel_context_to_named_context : Environ.env -> types ->
+  named_context_val * types * constr list * csubst * (identifier*constr) list
 
-val generalize_evar_over_rels : evar_map -> EConstr.existential -> EConstr.types * EConstr.constr list
+val generalize_evar_over_rels : evar_map -> existential -> types * constr list
 
 (** Evar combinators *)
 
@@ -235,5 +236,5 @@ val meta_counter_summary_name : string
 
 (** Deprecater *)
 
-type type_constraint = EConstr.types option
-type val_constraint = EConstr.constr option
+type type_constraint = types option
+type val_constraint = constr option