Imported Upstream version 8.5~beta1+dfsg

1 files changed, 173 insertions, 328 deletions

diff --git a/kernel/term.mli b/kernel/term.mli
index 33d3daaf..501aaf74 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -1,237 +1,101 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Names
+open Context
 
+(** {5 Redeclaration of types from module Constr and Sorts}
 
-(** {6 The sorts of CCI. } *)
+    This reexports constructors of inductive types defined in module [Constr],
+    for compatibility purposes. Refer to this module for further info.
 
-type contents = Pos | Null
+*)
+
+type contents = Sorts.contents = Pos | Null
 
-type sorts =
+type sorts = Sorts.t =
   | Prop of contents       (** Prop and Set *)
   | Type of Univ.universe  (** Type *)
 
-val set_sort  : sorts
-val prop_sort : sorts
-val type1_sort  : sorts
+type sorts_family = Sorts.family = InProp | InSet | InType
 
-(** {6 The sorts family of CCI. } *)
+type 'a puniverses = 'a Univ.puniverses
 
-type sorts_family = InProp | InSet | InType
+(** Simply type aliases *)
+type pconstant = constant puniverses
+type pinductive = inductive puniverses
+type pconstructor = constructor puniverses
 
-val family_of_sort : sorts -> sorts_family
+type constr = Constr.constr
+(** Alias types, for compatibility. *)
+
+type types = Constr.types
+(** Same as [constr], for documentation purposes. *)
 
-(** {6 Useful types } *)
+type existential_key = Constr.existential_key
 
-(** {6 Existential variables } *)
-type existential_key = int
+type existential = Constr.existential
 
-(** {6 Existential variables } *)
-type metavariable = int
+type metavariable = Constr.metavariable
 
-(** {6 Case annotation } *)
-type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle 
-  | RegularStyle (** infer printing form from number of constructor *)
-type case_printing =
-  { ind_nargs : int; (** length of the arity of the inductive type *)
-    style     : case_style }
+type case_style = Constr.case_style =
+  LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 
-(** the integer is the number of real args, needed for reduction *)
-type case_info =
+type case_printing = Constr.case_printing =
+  { ind_tags : bool list; cstr_tags : bool list array; style : case_style }
+
+type case_info = Constr.case_info =
   { ci_ind        : inductive;
     ci_npar       : int;
-    ci_cstr_ndecls : int array; (** number of real args of each constructor *)
-    ci_pp_info    : case_printing (** not interpreted by the kernel *)
+    ci_cstr_ndecls : int array;
+    ci_cstr_nargs : int array;
+    ci_pp_info    : case_printing
   }
 
-(** {6 The type of constructions } *)
-
-type constr
-
-(** [eq_constr a b] is true if [a] equals [b] modulo alpha, casts,
-   and application grouping *)
-val eq_constr : constr -> constr -> bool
-
-(** [types] is the same as [constr] but is intended to be used for
-   documentation to indicate that such or such function specifically works
-   with {e types} (i.e. terms of type a sort).
-   (Rem:plurial form since [type] is a reserved ML keyword) *)
-
-type types = constr
-
-(** {5 Functions for dealing with constr terms. }
-  The following functions are intended to simplify and to uniform the
-  manipulation of terms. Some of these functions may be overlapped with
-  previous ones. *)
-
-(** {6 Term constructors. } *)
-
-(** Constructs a DeBrujin index (DB indices begin at 1) *)
-val mkRel : int -> constr
-
-(** Constructs a Variable *)
-val mkVar : identifier -> constr
-
-(** Constructs an patvar named "?n" *)
-val mkMeta : metavariable -> constr
-
-(** Constructs an existential variable *)
-type existential = existential_key * constr array
-val mkEvar : existential -> constr
-
-(** Construct a sort *)
-val mkSort : sorts -> types
-val mkProp : types
-val mkSet  : types
-val mkType : Univ.universe -> types
-
-
-(** This defines the strategy to use for verifiying a Cast *)
-type cast_kind = VMcast | DEFAULTcast | REVERTcast
-
-(** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the
-   type t{_ 2} (that means t2 is declared as the type of t1). *)
-val mkCast : constr * cast_kind * constr -> constr
-
-(** Constructs the product [(x:t1)t2] *)
-val mkProd : name * types * types -> types
-val mkNamedProd : identifier -> types -> types -> types
+type cast_kind = Constr.cast_kind =
+  VMcast | NATIVEcast | DEFAULTcast | REVERTcast
 
-(** non-dependent product [t1 -> t2], an alias for
-   [forall (_:t1), t2]. Beware [t_2] is NOT lifted.
-   Eg: in context [A:Prop], [A->A] is built by [(mkArrow (mkRel 0) (mkRel 1))]
-*)
-val mkArrow : types -> types -> constr
-
-(** Constructs the abstraction \[x:t{_ 1}\]t{_ 2} *)
-val mkLambda : name * types * constr -> constr
-val mkNamedLambda : identifier -> types -> constr -> constr
-
-(** Constructs the product [let x = t1 : t2 in t3] *)
-val mkLetIn : name * constr * types * constr -> constr
-val mkNamedLetIn : identifier -> constr -> types -> constr -> constr
-
-(** [mkApp (f,[| t_1; ...; t_n |]] constructs the application
-   {% $(f~t_1~\dots~t_n)$ %}. *)
-val mkApp : constr * constr array -> constr
-
-(** Constructs a constant 
-   The array of terms correspond to the variables introduced in the section *)
-val mkConst : constant -> constr
-
-(** Inductive types *)
-
-(** Constructs the ith (co)inductive type of the block named kn 
-   The array of terms correspond to the variables introduced in the section *)
-val mkInd : inductive -> constr
-
-(** Constructs the jth constructor of the ith (co)inductive type of the
-   block named kn. The array of terms correspond to the variables
-   introduced in the section *)
-val mkConstruct : constructor -> constr
-
-(** Constructs a destructor of inductive type.
-    
-    [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] 
-    presented as describe in [ci].
-
-    [p] stucture is [fun args x -> "return clause"]
-
-    [ac]{^ ith} element is ith constructor case presented as 
-    {e lambda construct_args (without params). case_term } *)
-val mkCase : case_info * constr * constr * constr array -> constr
-
-(** If [recindxs = [|i1,...in|]]
-      [funnames = [|f1,.....fn|]]
-      [typarray = [|t1,...tn|]]
-      [bodies   = [|b1,.....bn|]]
-   then [mkFix ((recindxs,i), funnames, typarray, bodies) ]
-   constructs the {% $ %}i{% $ %}th function of the block (counting from 0)
-
-    [Fixpoint f1 [ctx1] = b1
-     with     f2 [ctx2] = b2
-     ...
-     with     fn [ctxn] = bn.]
-
-   where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
-*)
-type rec_declaration = name array * types array * constr array
-type fixpoint = (int array * int) * rec_declaration
-val mkFix : fixpoint -> constr
-
-(** If [funnames = [|f1,.....fn|]]
-      [typarray = [|t1,...tn|]]
-      [bodies   = [b1,.....bn]] 
-   then [mkCoFix (i, (funnames, typarray, bodies))]
-   constructs the ith function of the block
-   
-    [CoFixpoint f1 = b1
-     with       f2 = b2
-     ...
-     with       fn = bn.]
- *)
-type cofixpoint = int * rec_declaration
-val mkCoFix : cofixpoint -> constr
-
-
-(** {6 Concrete type for making pattern-matching. } *)
-
-(** [constr array] is an instance matching definitional [named_context] in
-   the same order (i.e. last argument first) *)
-type 'constr pexistential = existential_key * 'constr array
+type rec_declaration = Constr.rec_declaration
+type fixpoint = Constr.fixpoint
+type cofixpoint = Constr.cofixpoint
+type 'constr pexistential = 'constr Constr.pexistential
 type ('constr, 'types) prec_declaration =
-    name array * 'types array * 'constr array
-type ('constr, 'types) pfixpoint =
-    (int array * int) * ('constr, 'types) prec_declaration
-type ('constr, 'types) pcofixpoint =
-    int * ('constr, 'types) prec_declaration
+  ('constr, 'types) Constr.prec_declaration
+type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint
+type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint
 
-type ('constr, 'types) kind_of_term =
+type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term =
   | Rel       of int
-  | Var       of identifier
+  | Var       of Id.t
   | Meta      of metavariable
   | Evar      of 'constr pexistential
   | Sort      of sorts
   | Cast      of 'constr * cast_kind * 'types
-  | Prod      of name * 'types * 'types
-  | Lambda    of name * 'types * 'constr
-  | LetIn     of name * 'constr * 'types * 'constr
+  | Prod      of Name.t * 'types * 'types
+  | Lambda    of Name.t * 'types * 'constr
+  | LetIn     of Name.t * 'constr * 'types * 'constr
   | App       of 'constr * 'constr array
-  | Const     of constant
-  | Ind       of inductive
-  | Construct of constructor
+  | Const     of constant puniverses
+  | Ind       of inductive puniverses
+  | Construct of constructor puniverses
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
+  | Proj      of projection * 'constr
 
-(** User view of [constr]. For [App], it is ensured there is at
-   least one argument and the function is not itself an applicative
-   term *)
+type values = Constr.values
 
-val kind_of_term : constr -> (constr, types) kind_of_term
-
-(** Experimental, used in Presburger contrib *)
-type ('constr, 'types) kind_of_type =
-  | SortType   of sorts
-  | CastType   of 'types * 'types
-  | ProdType   of name * 'types * 'types
-  | LetInType  of name * 'constr * 'types * 'types
-  | AtomicType of 'constr * 'constr array
-
-val kind_of_type : types -> (constr, types) kind_of_type
-
-(** {6 Simple term case analysis. } *)
+(** {5 Simple term case analysis. } *)
 
 val isRel  : constr -> bool
 val isRelN : int -> constr -> bool
 val isVar  : constr -> bool
-val isVarId : identifier -> constr -> bool
+val isVarId : Id.t -> constr -> bool
 val isInd  : constr -> bool
 val isEvar : constr -> bool
 val isMeta : constr -> bool
@@ -248,6 +112,7 @@ val isConstruct : constr -> bool
 val isFix : constr -> bool
 val isCoFix : constr -> bool
 val isCase : constr -> bool
+val isProj : constr -> bool
 
 val is_Prop : constr -> bool
 val is_Set  : constr -> bool
@@ -257,9 +122,11 @@ val iskind : constr -> bool
 val is_small : sorts -> bool
 
 
-(** {6 Term destructors } *)
+(** {5 Term destructors } *)
 (** Destructor operations are partial functions and
-    @raise Invalid_argument "dest*" if the term has not the expected form. *)
+    @raise DestKO if the term has not the expected form. *)
+
+exception DestKO
 
 (** Destructs a DeBrujin index *)
 val destRel : constr -> int
@@ -268,7 +135,7 @@ val destRel : constr -> int
 val destMeta : constr -> metavariable
 
 (** Destructs a variable *)
-val destVar : constr -> identifier
+val destVar : constr -> Id.t
 
 (** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether
    [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *)
@@ -278,13 +145,13 @@ val destSort : constr -> sorts
 val destCast : constr -> constr * cast_kind * constr
 
 (** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *)
-val destProd : types -> name * types * types
+val destProd : types -> Name.t * types * types
 
 (** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *)
-val destLambda : constr -> name * types * constr
+val destLambda : constr -> Name.t * types * constr
 
 (** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *)
-val destLetIn : constr -> name * constr * types * constr
+val destLetIn : constr -> Name.t * constr * types * constr
 
 (** Destructs an application *)
 val destApp : constr -> constr * constr array
@@ -295,17 +162,20 @@ val destApplication : constr -> constr * constr array
 (** Decompose any term as an applicative term; the list of args can be empty *)
 val decompose_app : constr -> constr * constr list
 
+(** Same as [decompose_app], but returns an array. *)
+val decompose_appvect : constr -> constr * constr array
+
 (** Destructs a constant *)
-val destConst : constr -> constant
+val destConst : constr -> constant puniverses
 
 (** Destructs an existential variable *)
 val destEvar : constr -> existential
 
 (** Destructs a (co)inductive type *)
-val destInd : constr -> inductive
+val destInd : constr -> inductive puniverses
 
 (** Destructs a constructor *)
-val destConstruct : constr -> constructor
+val destConstruct : constr -> constructor puniverses
 
 (** Destructs a [match c as x in I args return P with ... |
 Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args
@@ -314,6 +184,9 @@ return P in t1], or [if c then t1 else t2])
 where [info] is pretty-printing information *)
 val destCase : constr -> case_info * constr * constr * constr array
 
+(** Destructs a projection *)
+val destProj : constr -> projection * constr
+
 (** Destructs the {% $ %}i{% $ %}th function of the block
    [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1}
     with    f{_ 2} ctx{_ 2} = b{_ 2}
@@ -326,54 +199,18 @@ val destFix : constr -> fixpoint
 val destCoFix : constr -> cofixpoint
 
 
-(** {6 Local } *)
-(** A {e declaration} has the form [(name,body,type)]. It is either an
-    {e assumption} if [body=None] or a {e definition} if
-    [body=Some actualbody]. It is referred by {e name} if [na] is an
-    identifier or by {e relative index} if [na] is not an identifier
-    (in the latter case, [na] is of type [name] but just for printing
-    purpose) *)
-
-type named_declaration = identifier * constr option * types
-type rel_declaration = name * constr option * types
-
-val map_named_declaration :
-  (constr -> constr) -> named_declaration -> named_declaration
-val map_rel_declaration :
-  (constr -> constr) -> rel_declaration -> rel_declaration
-
-val fold_named_declaration :
-  (constr -> 'a -> 'a) -> named_declaration -> 'a -> 'a
-val fold_rel_declaration :
-  (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
-
-val exists_named_declaration :
-  (constr -> bool) -> named_declaration -> bool
-val exists_rel_declaration :
-  (constr -> bool) -> rel_declaration -> bool
-
-val for_all_named_declaration :
-  (constr -> bool) -> named_declaration -> bool
-val for_all_rel_declaration :
-  (constr -> bool) -> rel_declaration -> bool
+(** {5 Derived constructors} *)
 
-val eq_named_declaration :
-  named_declaration -> named_declaration -> bool
-
-val eq_rel_declaration :
-    rel_declaration -> rel_declaration -> bool
-
-(** {6 Contexts of declarations referred to by de Bruijn indices } *)
-
-(** In [rel_context], more recent declaration is on top *)
-type rel_context = rel_declaration list
-
-val empty_rel_context : rel_context
-val add_rel_decl : rel_declaration -> rel_context -> rel_context
+(** non-dependent product [t1 -> t2], an alias for
+   [forall (_:t1), t2]. Beware [t_2] is NOT lifted.
+   Eg: in context [A:Prop], [A->A] is built by [(mkArrow (mkRel 0) (mkRel 1))]
+*)
+val mkArrow : types -> types -> constr
 
-val lookup_rel : int -> rel_context -> rel_declaration
-val rel_context_length : rel_context -> int
-val rel_context_nhyps : rel_context -> int
+(** Named version of the functions from [Term]. *)
+val mkNamedLambda : Id.t -> types -> constr -> constr
+val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr
+val mkNamedProd : Id.t -> types -> types -> types
 
 (** Constructs either [(x:t)c] or [[x=b:t]c] *)
 val mkProd_or_LetIn : rel_declaration -> types -> types
@@ -385,7 +222,7 @@ val mkNamedProd_wo_LetIn : named_declaration -> types -> types
 val mkLambda_or_LetIn : rel_declaration -> constr -> constr
 val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr
 
-(** {6 Other term constructors. } *)
+(** {5 Other term constructors. } *)
 
 (** [applist (f,args)] and its variants work as [mkApp] *)
 
@@ -396,24 +233,24 @@ val appvectc : constr -> constr array -> constr
 
 (** [prodn n l b] = [forall (x_1:T_1)...(x_n:T_n), b]
    where [l] is [(x_n,T_n)...(x_1,T_1)...]. *)
-val prodn : int -> (name * constr) list -> constr -> constr
+val prodn : int -> (Name.t * constr) list -> constr -> constr
 
 (** [compose_prod l b]
    @return [forall (x_1:T_1)...(x_n:T_n), b]
    where [l] is [(x_n,T_n)...(x_1,T_1)].
    Inverse of [decompose_prod]. *)
-val compose_prod : (name * constr) list -> constr -> constr
+val compose_prod : (Name.t * constr) list -> constr -> constr
 
 (** [lamn n l b]
     @return [fun (x_1:T_1)...(x_n:T_n) => b]
    where [l] is [(x_n,T_n)...(x_1,T_1)...]. *)
-val lamn : int -> (name * constr) list -> constr -> constr
+val lamn : int -> (Name.t * constr) list -> constr -> constr
 
 (** [compose_lam l b]
    @return [fun (x_1:T_1)...(x_n:T_n) => b]
    where [l] is [(x_n,T_n)...(x_1,T_1)].
    Inverse of [it_destLam] *)
-val compose_lam : (name * constr) list -> constr -> constr
+val compose_lam : (Name.t * constr) list -> constr -> constr
 
 (** [to_lambda n l]
    @return [fun (x_1:T_1)...(x_n:T_n) => T]
@@ -434,24 +271,24 @@ val prod_applist : constr -> constr list -> constr
 val it_mkLambda_or_LetIn : constr -> rel_context -> constr
 val it_mkProd_or_LetIn : types -> rel_context -> types
 
-(** {6 Other term destructors. } *)
+(** {5 Other term destructors. } *)
 
 (** Transforms a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} into the pair
    {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a product. *)
-val decompose_prod : constr -> (name*constr) list * constr
+val decompose_prod : constr -> (Name.t*constr) list * constr
 
 (** Transforms a lambda term {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair
    {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a lambda. *)
-val decompose_lam : constr -> (name*constr) list * constr
+val decompose_lam : constr -> (Name.t*constr) list * constr
 
 (** Given a positive integer n, transforms a product term
    {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %}
    into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}. *)
-val decompose_prod_n : int -> constr -> (name * constr) list * constr
+val decompose_prod_n : int -> constr -> (Name.t * constr) list * constr
 
 (** Given a positive integer {% $ %}n{% $ %}, transforms a lambda term
    {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %} *)
-val decompose_lam_n : int -> constr -> (name * constr) list * constr
+val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr
 
 (** Extract the premisses and the conclusion of a term of the form
    "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *)
@@ -505,7 +342,7 @@ val under_casts : (constr -> constr) -> constr -> constr
 (** Apply a function under components of Cast if any *)
 val under_outer_cast : (constr -> constr) -> constr -> constr
 
-(** {6 ... } *)
+(** {5 ... } *)
 (** An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort.
     Such a term can canonically be seen as the pair of a context of types
     and of a sort *)
@@ -521,117 +358,125 @@ val destArity : types -> arity
 (** Tells if a term has the form of an arity *)
 val isArity : types -> bool
 
-(** {6 Occur checks } *)
+(** {5 Kind of type} *)
+
+type ('constr, 'types) kind_of_type =
+  | SortType   of sorts
+  | CastType   of 'types * 'types
+  | ProdType   of Name.t * 'types * 'types
+  | LetInType  of Name.t * 'constr * 'types * 'types
+  | AtomicType of 'constr * 'constr array
+
+val kind_of_type : types -> (constr, types) kind_of_type
 
-(** [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *)
-val closedn : int -> constr -> bool
+(** {5 Redeclaration of stuff from module [Sorts]} *)
 
-(** [closed0 M] is true iff [M] is a (deBruijn) closed term *)
-val closed0 : constr -> bool
+val set_sort  : sorts
+(** Alias for Sorts.set *)
 
-(** [noccurn n M] returns true iff [Rel n] does NOT occur in term [M]  *)
-val noccurn : int -> constr -> bool
+val prop_sort : sorts
+(** Alias for Sorts.prop *)
 
-(** [noccur_between n m M] returns true iff [Rel p] does NOT occur in term [M]
-  for n <= p < n+m *)
-val noccur_between : int -> int -> constr -> bool
+val type1_sort  : sorts
+(** Alias for Sorts.type1 *)
 
-(** Checking function for terms containing existential- or
-   meta-variables.  The function [noccur_with_meta] does not consider
-   meta-variables applied to some terms (intended to be its local
-   context) (for existential variables, it is necessarily the case) *)
-val noccur_with_meta : int -> int -> constr -> bool
+val sorts_ord : sorts -> sorts -> int
+(** Alias for Sorts.compare *)
 
-(** {6 Relocation and substitution } *)
+val is_prop_sort : sorts -> bool
+(** Alias for Sorts.is_prop *)
 
-(** [exliftn el c] lifts [c] with lifting [el] *)
-val exliftn : Esubst.lift -> constr -> constr
+val family_of_sort : sorts -> sorts_family
+(** Alias for Sorts.family *)
 
-(** [liftn n k c] lifts by [n] indexes above or equal to [k] in [c] *)
-val liftn : int -> int -> constr -> constr
+(** {5 Redeclaration of stuff from module [Constr]}
 
-(** [lift n c] lifts by [n] the positive indexes in [c] *)
-val lift : int -> constr -> constr
+    See module [Constr] for further info. *)
 
-(** [substnl [a1;...;an] k c] substitutes in parallel [a1],...,[an]
-    for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates
-    accordingly indexes in [a1],...,[an] *)
-val substnl : constr list -> int -> constr -> constr
-val substl : constr list -> constr -> constr
-val subst1 : constr -> constr -> constr
+(** {6 Term constructors. } *)
 
-val substnl_decl : constr list -> int -> rel_declaration -> rel_declaration
-val substl_decl : constr list -> rel_declaration -> rel_declaration
-val subst1_decl : constr -> rel_declaration -> rel_declaration
+val mkRel : int -> constr
+val mkVar : Id.t -> constr
+val mkMeta : metavariable -> constr
+val mkEvar : existential -> constr
+val mkSort : sorts -> types
+val mkProp : types
+val mkSet  : types
+val mkType : Univ.universe -> types
+val mkCast : constr * cast_kind * constr -> constr
+val mkProd : Name.t * types * types -> types
+val mkLambda : Name.t * types * constr -> constr
+val mkLetIn : Name.t * constr * types * constr -> constr
+val mkApp : constr * constr array -> constr
+val mkConst : constant -> constr
+val mkProj : projection * constr -> constr
+val mkInd : inductive -> constr
+val mkConstruct : constructor -> constr
+val mkConstU : constant puniverses -> constr
+val mkIndU : inductive puniverses -> constr
+val mkConstructU : constructor puniverses -> constr
+val mkConstructUi : (pinductive * int) -> constr
+val mkCase : case_info * constr * constr * constr array -> constr
+val mkFix : fixpoint -> constr
+val mkCoFix : cofixpoint -> constr
 
-val subst1_named_decl : constr -> named_declaration -> named_declaration
-val substl_named_decl : constr list -> named_declaration -> named_declaration
+(** {6 Aliases} *)
 
-val replace_vars : (identifier * constr) list -> constr -> constr
-val subst_var : identifier -> constr -> constr
+val eq_constr : constr -> constr -> bool
+(** Alias for [Constr.equal] *)
 
-(** [subst_vars [id1;...;idn] t] substitute [VAR idj] by [Rel j] in [t]
-   if two names are identical, the one of least indice is kept *)
-val subst_vars : identifier list -> constr -> constr
+(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
+   application grouping and the universe constraints in [u]. *)
+val eq_constr_univs : constr Univ.check_function
 
-(** [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t]
-   if two names are identical, the one of least indice is kept *)
-val substn_vars : int -> identifier list -> constr -> constr
+(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo 
+    alpha, casts, application grouping and the universe constraints in [u]. *)
+val leq_constr_univs : constr Univ.check_function
 
+(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts,
+   application grouping and ignoring universe instances. *)
+val eq_constr_nounivs : constr -> constr -> bool
 
-(** {6 Functionals working on the immediate subterm of a construction } *)
+val kind_of_term : constr -> (constr, types) kind_of_term
+(** Alias for [Constr.kind] *)
 
-(** [fold_constr f acc c] folds [f] on the immediate subterms of [c]
-   starting from [acc] and proceeding from left to right according to
-   the usual representation of the constructions; it is not recursive *)
+val constr_ord : constr -> constr -> int
+(** Alias for [Constr.compare] *)
 
 val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a
-
-(** [map_constr f c] maps [f] on the immediate subterms of [c]; it is
-   not recursive and the order with which subterms are processed is
-   not specified *)
+(** Alias for [Constr.fold] *)
 
 val map_constr : (constr -> constr) -> constr -> constr
-
-(** [map_constr_with_binders g f n c] maps [f n] on the immediate
-   subterms of [c]; it carries an extra data [n] (typically a lift
-   index) which is processed by [g] (which typically add 1 to [n]) at
-   each binder traversal; it is not recursive and the order with which
-   subterms are processed is not specified *)
+(** Alias for [Constr.map] *)
 
 val map_constr_with_binders :
   ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
+(** Alias for [Constr.map_with_binders] *)
 
-(** [iter_constr f c] iters [f] on the immediate subterms of [c]; it is
-   not recursive and the order with which subterms are processed is
-   not specified *)
+val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses
+val univ_of_sort : sorts -> Univ.universe
+val sort_of_univ : Univ.universe -> sorts
 
 val iter_constr : (constr -> unit) -> constr -> unit
-
-(** [iter_constr_with_binders g f n c] iters [f n] on the immediate
-   subterms of [c]; it carries an extra data [n] (typically a lift
-   index) which is processed by [g] (which typically add 1 to [n]) at
-   each binder traversal; it is not recursive and the order with which
-   subterms are processed is not specified *)
+(** Alias for [Constr.iter] *)
 
 val iter_constr_with_binders :
   ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
-
-(** [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare
-   the immediate subterms of [c1] of [c2] if needed; Cast's, binders
-   name and Cases annotations are not taken into account *)
+(** Alias for [Constr.iter_with_binders] *)
 
 val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
+(** Alias for [Constr.compare_head] *)
 
-val constr_ord : constr -> constr -> int
 val hash_constr : constr -> int
+(** Alias for [Constr.hash] *)
 
 (*********************************************************************)
 
 val hcons_sorts : sorts -> sorts
-val hcons_constr : constr -> constr
-val hcons_types : types -> types
+(** Alias for [Constr.hashcons_sorts] *)
 
-(**************************************)
+val hcons_constr : constr -> constr
+(** Alias for [Constr.hashcons] *)
 
-type values
+val hcons_types : types -> types
+(** Alias for [Constr.hashcons] *)