Removing some return type compatibility layers in Termops.

4 files changed, 141 insertions, 141 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 73286f2c4..8940be09d 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -47,10 +47,11 @@ let evd_comb2 f evdref x y =
     z
 
 let e_new_global evdref x = 
-  evd_comb1 (Evd.fresh_global (Global.env())) evdref x
+  EConstr.of_constr (evd_comb1 (Evd.fresh_global (Global.env())) evdref x)
 
 let new_global evd x = 
-  Sigma.fresh_global (Global.env()) evd x
+  let Sigma (c, sigma, p) = Sigma.fresh_global (Global.env()) evd x in
+  Sigma (EConstr.of_constr c, sigma, p)
 
 (****************************************************)
 (* Expanding/testing/exposing existential variables *)
@@ -230,7 +231,7 @@ let new_meta =
   let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in
   fun () -> incr meta_ctr; !meta_ctr
 
-let mk_new_meta () = mkMeta(new_meta())
+let mk_new_meta () = EConstr.mkMeta(new_meta())
 
 (* The list of non-instantiated existential declarations (order is important) *)
 
@@ -396,6 +397,7 @@ let default_source = (Loc.ghost,Evar_kinds.InternalHole)
 
 let restrict_evar evd evk filter candidates =
   let evd = Sigma.to_evar_map evd in
+  let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
   let evd, evk' = Evd.restrict evk filter ?candidates evd in
   Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd)
 
@@ -408,6 +410,7 @@ let new_pure_evar_full evd evi =
 let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ =
   let typ = EConstr.Unsafe.to_constr typ in
   let evd = Sigma.to_evar_map evd in
+  let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
   let default_naming = Misctypes.IntroAnonymous in
   let naming = Option.default default_naming naming in
   let evi = {
@@ -437,7 +440,7 @@ let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?prin
 (* Converting the env into the sign of the evar to define *)
 let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
   let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
-  let map c = EConstr.Unsafe.to_constr (subst2 subst vsubst (EConstr.of_constr c)) in
+  let map c = subst2 subst vsubst c in
   let candidates = Option.map (fun l -> List.map map l) candidates in
   let instance =
     match filter with
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 5882f02b9..ea9599c8b 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -17,18 +17,18 @@ open Environ
 
 (** [new_meta] is a generator of unique meta variables *)
 val new_meta : unit -> metavariable
-val mk_new_meta : unit -> constr
+val mk_new_meta : unit -> EConstr.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:constr list -> ?store:Store.t ->
+  ?candidates:EConstr.constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool -> EConstr.types -> (EConstr.constr, 'r) Sigma.sigma
 
 val new_pure_evar :
   named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
-  ?candidates:constr list -> ?store:Store.t ->
+  ?candidates:EConstr.constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool -> EConstr.types -> (evar, 'r) Sigma.sigma
 
@@ -37,7 +37,7 @@ 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:constr list -> ?store:Store.t ->
+  ?candidates:EConstr.constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool -> EConstr.types -> EConstr.constr
 
@@ -56,12 +56,12 @@ val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (EConstr.constr, 'r) Sigma.s
 val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> EConstr.constr
 
 val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t ->
-  constr list option -> (existential_key, 'r) Sigma.sigma
+  EConstr.constr list option -> (existential_key, 'r) Sigma.sigma
 
 (** Polymorphic constants *)
 
-val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma
-val e_new_global : evar_map ref -> Globnames.global_reference -> constr
+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
 
 (** 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
@@ -71,7 +71,7 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr
    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:constr list ->
+  ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:EConstr.constr list ->
   ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool ->
   EConstr.constr list -> (EConstr.constr, 'r) Sigma.sigma
diff --git a/engine/termops.ml b/engine/termops.ml
index 879d77de2..465832c10 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -210,12 +210,7 @@ let lookup_rel_id id sign =
   lookrec 1 sign
 
 (* Constructs either [forall x:t, c] or [let x:=b:t in c] *)
-let mkProd_or_LetIn decl c =
-  let open RelDecl in
-  match decl with
-    | LocalAssum (na,t) -> mkProd (na, t, c)
-    | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
-
+let mkProd_or_LetIn = EConstr.mkProd_or_LetIn
 (* Constructs either [forall x:t, c] or [c] in which [x] is replaced by [b] *)
 let mkProd_wo_LetIn decl c =
   let open EConstr in
@@ -628,9 +623,10 @@ let vars_of_global_reference env gr =
    [m] is appropriately lifted through abstractions of [t] *)
 
 let dependent_main noevar univs sigma m t =
+  let open EConstr in
   let eqc x y =
-    if univs then not (Option.is_empty (EConstr.eq_constr_universes sigma x y))
-    else EConstr.eq_constr_nounivs sigma x y
+    if univs then not (Option.is_empty (eq_constr_universes sigma x y))
+    else eq_constr_nounivs sigma x y
   in
   let rec deprec m t =
     if eqc m t then
@@ -638,13 +634,13 @@ let dependent_main noevar univs sigma m t =
     else
       match EConstr.kind sigma m, EConstr.kind sigma t with
 	| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
-	    deprec m (EConstr.mkApp (ft,Array.sub lt 0 (Array.length lm)));
+	    deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
 	    CArray.Fun1.iter deprec m
 	      (Array.sub lt
 		(Array.length lm) ((Array.length lt) - (Array.length lm)))
-	| _, Cast (c,_,_) when noevar && EConstr.isMeta sigma c -> ()
+	| _, Cast (c,_,_) when noevar && isMeta sigma c -> ()
 	| _, Evar _ when noevar -> ()
-	| _ -> EConstr.iter_with_binders sigma (fun c -> EConstr.Vars.lift 1 c) deprec m t
+	| _ -> EConstr.iter_with_binders sigma (fun c -> Vars.lift 1 c) deprec m t
   in
   try deprec m t; false with Occur -> true
 
@@ -661,6 +657,7 @@ let dependent_in_decl sigma a decl =
     | LocalDef (_, body, t) -> dependent sigma a (EConstr.of_constr body) || dependent sigma a (EConstr.of_constr t)
 
 let count_occurrences sigma m t =
+  let open EConstr in
   let n = ref 0 in
   let rec countrec m t =
     if EConstr.eq_constr sigma m t then
@@ -668,13 +665,13 @@ let count_occurrences sigma m t =
     else
       match EConstr.kind sigma m, EConstr.kind sigma t with
 	| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
-	    countrec m (EConstr.mkApp (ft,Array.sub lt 0 (Array.length lm)));
+	    countrec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
 	    Array.iter (countrec m)
 	      (Array.sub lt
 		(Array.length lm) ((Array.length lt) - (Array.length lm)))
-	| _, Cast (c,_,_) when EConstr.isMeta sigma c -> ()
+	| _, Cast (c,_,_) when isMeta sigma c -> ()
 	| _, Evar _ -> ()
-	| _ -> EConstr.iter_with_binders sigma (EConstr.Vars.lift 1) countrec m t
+	| _ -> EConstr.iter_with_binders sigma (Vars.lift 1) countrec m t
   in
   countrec m t;
   !n
@@ -682,7 +679,7 @@ let count_occurrences sigma m t =
 (* Synonymous *)
 let occur_term = dependent
 
-let pop t = EConstr.Unsafe.to_constr (EConstr.Vars.lift (-1) t)
+let pop t = EConstr.Vars.lift (-1) t
 
 (***************************)
 (*  bindings functions *)
@@ -712,33 +709,35 @@ let collapse_appl sigma c = match EConstr.kind sigma c with
         | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
         | _ -> EConstr.mkApp (f,cl2)
       in
-      EConstr.Unsafe.to_constr (collapse_rec f cl)
-  | _ -> EConstr.Unsafe.to_constr c
+      collapse_rec f cl
+  | _ -> c
 
 (* First utilities for avoiding telescope computation for subst_term *)
 
 let prefix_application sigma eq_fun (k,c) t =
-  let c' = EConstr.of_constr (collapse_appl sigma c) and t' = EConstr.of_constr (collapse_appl sigma t) in
+  let open EConstr in
+  let c' = collapse_appl sigma c and t' = collapse_appl sigma t in
   match EConstr.kind sigma c', EConstr.kind sigma t' with
     | App (f1,cl1), App (f2,cl2) ->
 	let l1 = Array.length cl1
 	and l2 = Array.length cl2 in
 	if l1 <= l2
-	   && eq_fun sigma c' (EConstr.mkApp (f2, Array.sub cl2 0 l1)) then
-	  Some (EConstr.mkApp (EConstr.mkRel k, Array.sub cl2 l1 (l2 - l1)))
+	   && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then
+	  Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
 	else
 	  None
     | _ -> None
 
 let my_prefix_application sigma eq_fun (k,c) by_c t =
-  let c' = EConstr.of_constr (collapse_appl sigma c) and t' = EConstr.of_constr (collapse_appl sigma t) in
+  let open EConstr in
+  let c' = collapse_appl sigma c and t' = collapse_appl sigma t in
   match EConstr.kind sigma c', EConstr.kind sigma t' with
     | App (f1,cl1), App (f2,cl2) ->
 	let l1 = Array.length cl1
 	and l2 = Array.length cl2 in
 	if l1 <= l2
-	   && eq_fun sigma c' (EConstr.mkApp (f2, Array.sub cl2 0 l1)) then
-	  Some (EConstr.mkApp ((EConstr.Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1)))
+	   && eq_fun sigma c' (mkApp (f2, Array.sub cl2 0 l1)) then
+	  Some (mkApp ((Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1)))
 	else
 	  None
     | _ -> None
@@ -754,7 +753,7 @@ let subst_term_gen sigma eq_fun c t =
     match prefix_application sigma eq_fun kc t with
       | Some x -> x
       | None ->
-    if eq_fun sigma c t then EConstr.mkRel k
+    if eq_fun sigma c t then mkRel k
     else
       EConstr.map_with_binders sigma (fun (k,c) -> (k+1,lift 1 c)) substrec kc t
   in
@@ -775,7 +774,7 @@ let replace_term_gen sigma eq_fun c by_c in_t =
       EConstr.map_with_binders sigma (fun (k,c) -> (k+1,EConstr.Vars.lift 1 c))
 	substrec kc t)
   in
-  EConstr.Unsafe.to_constr (substrec (0,c) in_t)
+  substrec (0,c) in_t
 
 let replace_term sigma c byc t = replace_term_gen sigma EConstr.eq_constr c byc t
 
@@ -933,12 +932,11 @@ let filtering sigma env cv_pb c1 c2 =
   aux env cv_pb c1 c2; !evm
 
 let decompose_prod_letin sigma c =
-  let inj c = EConstr.Unsafe.to_constr c in
   let rec prodec_rec i l sigma c = match EConstr.kind sigma c with
-    | Prod (n,t,c)    -> prodec_rec (succ i) (RelDecl.LocalAssum (n, inj t)::l) sigma c
-    | LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n, inj d, inj t)::l) sigma c
+    | Prod (n,t,c)    -> prodec_rec (succ i) (local_assum (n, t)::l) sigma c
+    | LetIn (n,d,t,c) -> prodec_rec (succ i) (local_def (n, d, t)::l) sigma c
     | Cast (c,_,_)    -> prodec_rec i l sigma c
-    | _               -> i,l, inj c in
+    | _               -> i,l, c in
   prodec_rec 0 [] sigma c
 
 (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
@@ -969,7 +967,7 @@ let nb_prod_modulo_zeta sigma x =
       | _ -> n
   in count 0 x
 
-let align_prod_letin sigma c a : Context.Rel.t * constr =
+let align_prod_letin sigma c a =
   let (lc,_,_) = decompose_prod_letin sigma c in
   let (la,l,a) = decompose_prod_letin sigma a in
   if not (la >= lc) then invalid_arg "align_prod_letin";
@@ -980,21 +978,23 @@ let align_prod_letin sigma c a : Context.Rel.t * constr =
 (* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
 (* Remplace 2 earlier buggish versions                      *)
 
-let rec eta_reduce_head c =
-  match kind_of_term c with
+let rec eta_reduce_head sigma c =
+  let open EConstr in
+  let open Vars in
+  match EConstr.kind sigma c with
     | Lambda (_,c1,c') ->
-	(match kind_of_term (eta_reduce_head c') with
+	(match EConstr.kind sigma (eta_reduce_head sigma c') with
            | App (f,cl) ->
                let lastn = (Array.length cl) - 1 in
                if lastn < 0 then anomaly (Pp.str "application without arguments")
                else
-                 (match kind_of_term cl.(lastn) with
+                 (match EConstr.kind sigma cl.(lastn) with
                     | Rel 1 ->
 			let c' =
                           if Int.equal lastn 0 then f
 			  else mkApp (f, Array.sub cl 0 lastn)
 			in
-			if noccurn 1 c'
+			if noccurn sigma 1 c'
                         then lift (-1) c'
                         else c
                     | _   -> c)
diff --git a/engine/termops.mli b/engine/termops.mli
index 1699d600e..d7d9c743d 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -12,6 +12,7 @@
 open Pp
 open Names
 open Term
+open EConstr
 open Environ
 
 (** printers *)
@@ -20,59 +21,56 @@ val pr_sort_family : sorts_family -> std_ppcmds
 val pr_fix : ('a -> std_ppcmds) -> ('a, 'a) pfixpoint -> std_ppcmds
 
 (** debug printer: do not use to display terms to the casual user... *)
-val set_print_constr : (env -> constr -> std_ppcmds) -> unit
-val print_constr     : constr -> std_ppcmds
-val print_constr_env : env -> constr -> std_ppcmds
+val set_print_constr : (env -> Constr.constr -> std_ppcmds) -> unit
+val print_constr     : Constr.constr -> std_ppcmds
+val print_constr_env : env -> Constr.constr -> std_ppcmds
 val print_named_context : env -> std_ppcmds
 val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds
 val print_rel_context : env -> std_ppcmds
 val print_env : env -> std_ppcmds
 
 (** about contexts *)
-val push_rel_assum : Name.t * EConstr.types -> env -> env
-val push_rels_assum : (Name.t * types) list -> env -> env
-val push_named_rec_types : Name.t array * types array * 'a -> env -> env
+val push_rel_assum : Name.t * types -> env -> env
+val push_rels_assum : (Name.t * Constr.types) list -> env -> env
+val push_named_rec_types : Name.t array * Constr.types array * 'a -> env -> env
 
-val lookup_rel_id : Id.t -> Context.Rel.t -> int * constr option * types
+val lookup_rel_id : Id.t -> Context.Rel.t -> int * Constr.constr option * Constr.types
 (** Associates the contents of an identifier in a [rel_context]. Raise
     [Not_found] if there is no such identifier. *)
 
 (** Functions that build argument lists matching a block of binders or a context.
     [rel_vect n m] builds [|Rel (n+m);...;Rel(n+1)|]
 *)
-val rel_vect : int -> int -> constr array
-val rel_list : int -> int -> EConstr.constr list
+val rel_vect : int -> int -> Constr.constr array
+val rel_list : int -> int -> constr list
 
 (** iterators/destructors on terms *)
 val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
-val mkProd_wo_LetIn : Context.Rel.Declaration.t -> EConstr.types -> EConstr.types
-val it_mkProd : EConstr.types -> (Name.t * EConstr.types) list -> EConstr.types
-val it_mkLambda : EConstr.constr -> (Name.t * EConstr.types) list -> EConstr.constr
+val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types
+val it_mkProd : types -> (Name.t * types) list -> types
+val it_mkLambda : constr -> (Name.t * types) list -> constr
 val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
-val it_mkProd_wo_LetIn : EConstr.types -> Context.Rel.t -> EConstr.types
-val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
-val it_mkNamedProd_or_LetIn : EConstr.types -> Context.Named.t -> EConstr.types
-val it_mkNamedProd_wo_LetIn : types -> Context.Named.t -> types
-val it_mkNamedLambda_or_LetIn : EConstr.constr -> Context.Named.t -> EConstr.constr
+val it_mkProd_wo_LetIn : types -> Context.Rel.t -> types
+val it_mkLambda_or_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr
+val it_mkNamedProd_or_LetIn : types -> Context.Named.t -> types
+val it_mkNamedProd_wo_LetIn : Constr.types -> Context.Named.t -> Constr.types
+val it_mkNamedLambda_or_LetIn : constr -> Context.Named.t -> constr
 
 (* Ad hoc version reinserting letin, assuming the body is defined in
    the context where the letins are expanded *)
-val it_mkLambda_or_LetIn_from_no_LetIn : constr -> Context.Rel.t -> constr
+val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr
 
 (** {6 Generic iterators on constr} *)
 
-val map_constr_with_named_binders :
-  (Name.t -> 'a -> 'a) ->
-  ('a -> constr -> constr) -> 'a -> constr -> constr
 val map_constr_with_binders_left_to_right :
   Evd.evar_map ->
   (Context.Rel.Declaration.t -> 'a -> 'a) ->
-  ('a -> EConstr.constr -> EConstr.constr) ->
-    'a -> EConstr.constr -> EConstr.constr
+  ('a -> constr -> constr) ->
+    'a -> constr -> constr
 val map_constr_with_full_binders :
   Evd.evar_map ->
   (Context.Rel.Declaration.t -> 'a -> 'a) ->
-  ('a -> EConstr.t -> EConstr.t) -> 'a -> EConstr.t -> EConstr.t
+  ('a -> constr -> constr) -> 'a -> constr -> constr
 
 (** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
    subterms of [c] starting from [acc] and proceeding from left to
@@ -81,62 +79,61 @@ val map_constr_with_full_binders :
    index) which is processed by [g] (which typically add 1 to [n]) at
    each binder traversal; it is not recursive *)
 
-val fold_constr_with_binders :
-  Evd.evar_map -> ('a -> 'a) ->
-    ('a -> 'b -> EConstr.t -> 'b) -> 'a -> 'b -> EConstr.t -> 'b
+val fold_constr_with_binders : Evd.evar_map ->
+  ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
 
-val fold_constr_with_full_binders :
-  Evd.evar_map -> (Context.Rel.Declaration.t -> 'a -> 'a) ->
-    ('a -> 'b -> EConstr.t -> 'b) -> 'a -> 'b -> EConstr.t -> 'b
+val fold_constr_with_full_binders : Evd.evar_map ->
+  (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
+    'a -> 'b -> constr -> 'b
 
 val iter_constr_with_full_binders :
-  (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a ->
-    constr -> unit
+  (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> Constr.constr -> unit) -> 'a ->
+    Constr.constr -> unit
 
 (**********************************************************************)
 
-val strip_head_cast : Evd.evar_map -> EConstr.t -> EConstr.t
-val drop_extra_implicit_args : Evd.evar_map -> EConstr.t -> EConstr.constr
+val strip_head_cast : Evd.evar_map -> constr -> constr
+val drop_extra_implicit_args : Evd.evar_map -> constr -> constr
 
 (** occur checks *)
 
 exception Occur
-val occur_meta : Evd.evar_map -> EConstr.t -> bool
-val occur_existential : Evd.evar_map -> EConstr.t -> bool
-val occur_meta_or_existential : Evd.evar_map -> EConstr.t -> bool
-val occur_evar : Evd.evar_map -> existential_key -> EConstr.t -> bool
-val occur_var : env -> Evd.evar_map -> Id.t -> EConstr.t -> bool
+val occur_meta : Evd.evar_map -> constr -> bool
+val occur_existential : Evd.evar_map -> constr -> bool
+val occur_meta_or_existential : Evd.evar_map -> constr -> bool
+val occur_evar : Evd.evar_map -> existential_key -> constr -> bool
+val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool
 val occur_var_in_decl :
   env -> Evd.evar_map ->
   Id.t -> Context.Named.Declaration.t -> bool
 
 (** As {!occur_var} but assume the identifier not to be a section variable *)
-val local_occur_var : Evd.evar_map -> Id.t -> EConstr.t -> bool
+val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool
 
-val free_rels : Evd.evar_map -> EConstr.t -> Int.Set.t
+val free_rels : Evd.evar_map -> constr -> Int.Set.t
 
 (** [dependent m t] tests whether [m] is a subterm of [t] *)
-val dependent : Evd.evar_map -> EConstr.t -> EConstr.t -> bool
-val dependent_no_evar : Evd.evar_map -> EConstr.t -> EConstr.t -> bool
-val dependent_univs : Evd.evar_map -> EConstr.t -> EConstr.t -> bool
-val dependent_univs_no_evar : Evd.evar_map -> EConstr.t -> EConstr.t -> bool
-val dependent_in_decl : Evd.evar_map -> EConstr.t -> Context.Named.Declaration.t -> bool
-val count_occurrences : Evd.evar_map -> EConstr.t -> EConstr.t -> int
-val collect_metas : Evd.evar_map -> EConstr.t -> int list
-val collect_vars : Evd.evar_map -> EConstr.t -> Id.Set.t (** for visible vars only *)
+val dependent : Evd.evar_map -> constr -> constr -> bool
+val dependent_no_evar : Evd.evar_map -> constr -> constr -> bool
+val dependent_univs : Evd.evar_map -> constr -> constr -> bool
+val dependent_univs_no_evar : Evd.evar_map -> constr -> constr -> bool
+val dependent_in_decl : Evd.evar_map -> constr -> Context.Named.Declaration.t -> bool
+val count_occurrences : Evd.evar_map -> constr -> constr -> int
+val collect_metas : Evd.evar_map -> constr -> int list
+val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
 val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t
-val occur_term : Evd.evar_map -> EConstr.t -> EConstr.t -> bool (** Synonymous of dependent *)
+val occur_term : Evd.evar_map -> constr -> constr -> bool (** Synonymous of dependent *)
 
 (* Substitution of metavariables *)
-type meta_value_map = (metavariable * constr) list
-val subst_meta : meta_value_map -> constr -> constr
-val isMetaOf : Evd.evar_map -> metavariable -> EConstr.constr -> bool
+type meta_value_map = (metavariable * Constr.constr) list
+val subst_meta : meta_value_map -> Constr.constr -> Constr.constr
+val isMetaOf : Evd.evar_map -> metavariable -> constr -> bool
 
 (** Type assignment for metavariables *)
-type meta_type_map = (metavariable * types) list
+type meta_type_map = (metavariable * Constr.types) list
 
 (** [pop c] lifts by -1 the positive indexes in [c] *)
-val pop : EConstr.t -> constr
+val pop : constr -> constr
 
 (** {6 ... } *)
 (** Substitution of an arbitrary large term. Uses equality modulo
@@ -145,37 +142,37 @@ val pop : EConstr.t -> constr
 (** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq]
    as equality *)
 val subst_term_gen : Evd.evar_map ->
-  (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> EConstr.t -> EConstr.t -> EConstr.constr
+  (Evd.evar_map -> constr -> constr -> bool) -> constr -> constr -> constr
 
 (** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq]
    as equality *)
 val replace_term_gen :
-  Evd.evar_map -> (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) ->
-    EConstr.t -> EConstr.t -> EConstr.t -> constr
+  Evd.evar_map -> (Evd.evar_map -> constr -> constr -> bool) ->
+    constr -> constr -> constr -> constr
 
 (** [subst_term d c] replaces [d] by [Rel 1] in [c] *)
-val subst_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.constr
+val subst_term : Evd.evar_map -> constr -> constr -> constr
 
 (** [replace_term d e c] replaces [d] by [e] in [c] *)
-val replace_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.t -> constr
+val replace_term : Evd.evar_map -> constr -> constr -> constr -> constr
 
 (** Alternative term equalities *)
 val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool
-val compare_constr_univ : Evd.evar_map -> (Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool) ->
-  Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool
-val constr_cmp : Evd.evar_map -> Reduction.conv_pb -> EConstr.constr -> EConstr.constr -> bool
-val eq_constr : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool (* FIXME rename: erases universes*)
+val compare_constr_univ : Evd.evar_map -> (Reduction.conv_pb -> constr -> constr -> bool) ->
+  Reduction.conv_pb -> constr -> constr -> bool
+val constr_cmp : Evd.evar_map -> Reduction.conv_pb -> constr -> constr -> bool
+val eq_constr : Evd.evar_map -> constr -> constr -> bool (* FIXME rename: erases universes*)
 
-val eta_reduce_head : constr -> constr
+val eta_reduce_head : Evd.evar_map -> constr -> constr
 
 (** Flattens application lists *)
-val collapse_appl : Evd.evar_map -> EConstr.t -> constr
+val collapse_appl : Evd.evar_map -> constr -> constr
 
-val prod_applist : Evd.evar_map -> EConstr.t -> EConstr.t list -> EConstr.t
+val prod_applist : Evd.evar_map -> constr -> constr list -> constr
 
 (** Remove recursively the casts around a term i.e.
    [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
-val strip_outer_cast : Evd.evar_map -> EConstr.t -> EConstr.constr
+val strip_outer_cast : Evd.evar_map -> constr -> constr
 
 exception CannotFilter
 
@@ -185,32 +182,32 @@ exception CannotFilter
    (context,term), or raises [CannotFilter].
    Warning: Outer-kernel sort subtyping are taken into account: c1 has
    to be smaller than c2 wrt. sorts. *)
-type subst = (Context.Rel.t * constr) Evar.Map.t
-val filtering : Evd.evar_map -> Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst
+type subst = (Context.Rel.t * Constr.constr) Evar.Map.t
+val filtering : Evd.evar_map -> Context.Rel.t -> Reduction.conv_pb -> Constr.constr -> Constr.constr -> subst
 
-val decompose_prod_letin : Evd.evar_map -> EConstr.t -> int * Context.Rel.t * constr
-val align_prod_letin : Evd.evar_map -> EConstr.t -> EConstr.t -> Context.Rel.t * constr
+val decompose_prod_letin : Evd.evar_map -> constr -> int * Context.Rel.t * constr
+val align_prod_letin : Evd.evar_map -> constr -> constr -> Context.Rel.t * constr
 
 (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction
    gives {% $ %}n{% $ %} (casts are ignored) *)
-val nb_lam : Evd.evar_map -> EConstr.t -> int
+val nb_lam : Evd.evar_map -> constr -> int
 
 (** Similar to [nb_lam], but gives the number of products instead *)
-val nb_prod : Evd.evar_map -> EConstr.t -> int
+val nb_prod : Evd.evar_map -> constr -> int
 
 (** Similar to [nb_prod], but zeta-contracts let-in on the way *)
-val nb_prod_modulo_zeta : Evd.evar_map -> EConstr.t -> int
+val nb_prod_modulo_zeta : Evd.evar_map -> constr -> int
 
 (** Get the last arg of a constr intended to be an application *)
-val last_arg : Evd.evar_map -> EConstr.t -> EConstr.constr
+val last_arg : Evd.evar_map -> constr -> constr
 
 (** Force the decomposition of a term as an applicative one *)
-val decompose_app_vect : Evd.evar_map -> EConstr.t -> EConstr.constr * EConstr.constr array
+val decompose_app_vect : Evd.evar_map -> constr -> constr * constr array
 
-val adjust_app_list_size : EConstr.constr -> EConstr.constr list -> EConstr.constr -> EConstr.constr list ->
-  (EConstr.constr * EConstr.constr list * EConstr.constr * EConstr.constr list)
-val adjust_app_array_size : EConstr.constr -> EConstr.constr array -> EConstr.constr -> EConstr.constr array ->
-  (EConstr.constr * EConstr.constr array * EConstr.constr * EConstr.constr array)
+val adjust_app_list_size : constr -> constr list -> constr -> constr list ->
+  (constr * constr list * constr * constr list)
+val adjust_app_array_size : constr -> constr array -> constr -> constr array ->
+  (constr * constr array * constr * constr array)
 
 (** name contexts *)
 type names_context = Name.t list
@@ -239,15 +236,15 @@ val add_vname : Id.Set.t -> Name.t -> Id.Set.t
 
 (** other signature iterators *)
 val process_rel_context : (Context.Rel.Declaration.t -> env -> env) -> env -> env
-val assums_of_rel_context : Context.Rel.t -> (Name.t * constr) list
+val assums_of_rel_context : Context.Rel.t -> (Name.t * Constr.constr) list
 val lift_rel_context : int -> Context.Rel.t -> Context.Rel.t
-val substl_rel_context : constr list -> Context.Rel.t -> Context.Rel.t
+val substl_rel_context : Constr.constr list -> Context.Rel.t -> Context.Rel.t
 val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *)
 
 val map_rel_context_in_env :
-  (env -> constr -> constr) -> env -> Context.Rel.t -> Context.Rel.t
+  (env -> Constr.constr -> Constr.constr) -> env -> Context.Rel.t -> Context.Rel.t
 val map_rel_context_with_binders :
-  (int -> constr -> constr) -> Context.Rel.t -> Context.Rel.t
+  (int -> Constr.constr -> Constr.constr) -> Context.Rel.t -> Context.Rel.t
 val fold_named_context_both_sides :
   ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) ->
     Context.Named.t -> init:'a -> 'a
@@ -256,10 +253,10 @@ val compact_named_context : Context.Named.t -> Context.Compacted.t
 
 val clear_named_body : Id.t -> env -> env
 
-val global_vars : env -> Evd.evar_map -> EConstr.t -> Id.t list
-val global_vars_set : env -> Evd.evar_map -> EConstr.t -> Id.Set.t
+val global_vars : env -> Evd.evar_map -> constr -> Id.t list
+val global_vars_set : env -> Evd.evar_map -> constr -> Id.Set.t
 val global_vars_set_of_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Id.Set.t
-val global_app_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses * EConstr.constr option
+val global_app_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses * constr option
 
 (** Gives an ordered list of hypotheses, closed by dependencies,
    containing a given set *)
@@ -268,15 +265,15 @@ val dependency_closure : env -> Evd.evar_map -> Context.Named.t -> Id.Set.t -> I
 (** Test if an identifier is the basename of a global reference *)
 val is_section_variable : Id.t -> bool
 
-val global_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses
+val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses
 
-val is_global : Evd.evar_map -> Globnames.global_reference -> EConstr.constr -> bool
+val is_global : Evd.evar_map -> Globnames.global_reference -> constr -> bool
 
-val isGlobalRef : Evd.evar_map -> EConstr.t -> bool
+val isGlobalRef : Evd.evar_map -> constr -> bool
 
-val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool
+val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool
 
-val is_Prop : Evd.evar_map -> EConstr.t -> bool
+val is_Prop : Evd.evar_map -> constr -> bool
 
 (** Combinators on judgments *)
 
@@ -285,5 +282,5 @@ val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) puns
 val on_judgment_type  : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
 
 (** {6 Functions to deal with impossible cases } *)
-val set_impossible_default_clause : (unit -> (constr * types) Univ.in_universe_context_set) -> unit
+val set_impossible_default_clause : (unit -> (Constr.constr * Constr.types) Univ.in_universe_context_set) -> unit
 val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set