From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 30 Oct 2016 17:53:07 +0100
Subject: Termops API using EConstr.

---
 engine/termops.mli | 94 ++++++++++++++++++++++++++++--------------------------
 1 file changed, 48 insertions(+), 46 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 78826f79ae..5d53ce09e8 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -69,8 +69,9 @@ val map_constr_with_binders_left_to_right :
   ('a -> constr -> constr) ->
     'a -> constr -> constr
 val map_constr_with_full_binders :
+  Evd.evar_map ->
   (Context.Rel.Declaration.t -> 'a -> 'a) ->
-  ('a -> constr -> constr) -> 'a -> constr -> constr
+  ('a -> EConstr.t -> EConstr.t) -> 'a -> EConstr.t -> EConstr.t
 
 (** [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
@@ -80,11 +81,12 @@ val map_constr_with_full_binders :
    each binder traversal; it is not recursive *)
 
 val fold_constr_with_binders :
-  ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
+  Evd.evar_map -> ('a -> 'a) ->
+    ('a -> 'b -> EConstr.t -> 'b) -> 'a -> 'b -> EConstr.t -> 'b
 
 val fold_constr_with_full_binders :
-  (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
-    'a -> 'b -> constr -> 'b
+  Evd.evar_map -> (Context.Rel.Declaration.t -> 'a -> 'a) ->
+    ('a -> 'b -> EConstr.t -> 'b) -> 'a -> 'b -> EConstr.t -> 'b
 
 val iter_constr_with_full_binders :
   (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a ->
@@ -92,39 +94,39 @@ val iter_constr_with_full_binders :
 
 (**********************************************************************)
 
-val strip_head_cast : constr -> constr
-val drop_extra_implicit_args : constr -> constr
+val strip_head_cast : Evd.evar_map -> EConstr.t -> EConstr.t
+val drop_extra_implicit_args : Evd.evar_map -> EConstr.t -> constr
 
 (** occur checks *)
 
 exception Occur
-val occur_meta : types -> bool
-val occur_existential : types -> bool
-val occur_meta_or_existential : types -> bool
-val occur_evar : existential_key -> types -> bool
-val occur_var : env -> Id.t -> types -> bool
+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_var_in_decl :
-  env ->
+  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 : Id.t -> types -> bool
+val local_occur_var : Evd.evar_map -> Id.t -> EConstr.t -> bool
 
-val free_rels : constr -> Int.Set.t
+val free_rels : Evd.evar_map -> EConstr.t -> Int.Set.t
 
 (** [dependent m t] tests whether [m] is a subterm of [t] *)
-val dependent : constr -> constr -> bool
-val dependent_no_evar : constr -> constr -> bool
-val dependent_univs : constr -> constr -> bool
-val dependent_univs_no_evar : constr -> constr -> bool
-val dependent_in_decl : constr -> Context.Named.Declaration.t -> bool
-val count_occurrences : constr -> constr -> int
-val collect_metas : constr -> int list
-val collect_vars : constr -> Id.Set.t (** for visible vars only *)
+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 vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t
-val occur_term : constr -> constr -> bool (** Synonymous
- of dependent 
-   Substitution of metavariables *)
+val occur_term : Evd.evar_map -> EConstr.t -> EConstr.t -> bool (** Synonymous of dependent *)
+
+(* Substitution of metavariables *)
 type meta_value_map = (metavariable * constr) list
 val subst_meta : meta_value_map -> constr -> constr
 
@@ -132,7 +134,7 @@ val subst_meta : meta_value_map -> constr -> constr
 type meta_type_map = (metavariable * types) list
 
 (** [pop c] lifts by -1 the positive indexes in [c] *)
-val pop : constr -> constr
+val pop : EConstr.t -> constr
 
 (** {6 ... } *)
 (** Substitution of an arbitrary large term. Uses equality modulo
@@ -140,20 +142,20 @@ val pop : constr -> constr
 
 (** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq]
    as equality *)
-val subst_term_gen :
-  (constr -> constr -> bool) -> constr -> constr -> constr
+val subst_term_gen : Evd.evar_map ->
+  (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> EConstr.t -> EConstr.t -> constr
 
 (** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq]
    as equality *)
 val replace_term_gen :
-  (constr -> constr -> bool) ->
-    constr -> constr -> constr -> constr
+  Evd.evar_map -> (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) ->
+    EConstr.t -> EConstr.t -> EConstr.t -> constr
 
 (** [subst_term d c] replaces [d] by [Rel 1] in [c] *)
-val subst_term : constr -> constr -> constr
+val subst_term : Evd.evar_map -> EConstr.t -> EConstr.t -> constr
 
 (** [replace_term d e c] replaces [d] by [e] in [c] *)
-val replace_term : constr -> constr -> constr -> constr
+val replace_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.t -> constr
 
 (** Alternative term equalities *)
 val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool
@@ -165,11 +167,11 @@ val eq_constr : constr -> constr -> bool (* FIXME rename: erases universes*)
 val eta_reduce_head : constr -> constr
 
 (** Flattens application lists *)
-val collapse_appl : constr -> constr
+val collapse_appl : Evd.evar_map -> EConstr.t -> constr
 
 (** Remove recursively the casts around a term i.e.
    [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
-val strip_outer_cast : constr -> constr
+val strip_outer_cast : Evd.evar_map -> EConstr.t -> constr
 
 exception CannotFilter
 
@@ -182,24 +184,24 @@ exception CannotFilter
 type subst = (Context.Rel.t * constr) Evar.Map.t
 val filtering : Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst
 
-val decompose_prod_letin : constr -> int * Context.Rel.t * constr
-val align_prod_letin : constr -> constr -> Context.Rel.t * constr
+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
 
 (** [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 : constr -> int
+val nb_lam : Evd.evar_map -> EConstr.t -> int
 
 (** Similar to [nb_lam], but gives the number of products instead *)
-val nb_prod : constr -> int
+val nb_prod : Evd.evar_map -> EConstr.t -> int
 
 (** Similar to [nb_prod], but zeta-contracts let-in on the way *)
-val nb_prod_modulo_zeta : constr -> int
+val nb_prod_modulo_zeta : Evd.evar_map -> EConstr.t -> int
 
 (** Get the last arg of a constr intended to be an application *)
-val last_arg : constr -> constr
+val last_arg : Evd.evar_map -> EConstr.t -> constr
 
 (** Force the decomposition of a term as an applicative one *)
-val decompose_app_vect : constr -> constr * constr array
+val decompose_app_vect : Evd.evar_map -> EConstr.t -> constr * constr array
 
 val adjust_app_list_size : constr -> constr list -> constr -> constr list ->
   (constr * constr list * constr * constr list)
@@ -250,19 +252,19 @@ val compact_named_context : Context.Named.t -> Context.Compacted.t
 
 val clear_named_body : Id.t -> env -> env
 
-val global_vars : env -> constr -> Id.t list
-val global_vars_set_of_decl : env -> Context.Named.Declaration.t -> Id.Set.t
+val global_vars : env -> Evd.evar_map -> EConstr.t -> Id.t list
+val global_vars_set_of_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Id.Set.t
 
 (** Gives an ordered list of hypotheses, closed by dependencies,
    containing a given set *)
-val dependency_closure : env -> Context.Named.t -> Id.Set.t -> Id.t list
+val dependency_closure : env -> Evd.evar_map -> Context.Named.t -> Id.Set.t -> Id.t list
 
 (** Test if an identifier is the basename of a global reference *)
 val is_section_variable : Id.t -> bool
 
-val isGlobalRef : constr -> bool
+val isGlobalRef : Evd.evar_map -> EConstr.t -> bool
 
-val is_template_polymorphic : env -> constr -> bool
+val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool
 
 (** Combinators on judgments *)
 
-- 
cgit v1.2.3


From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Nov 2016 20:53:32 +0100
Subject: Reductionops API using EConstr.

---
 engine/termops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 5d53ce09e8..b536b0fb8b 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -17,7 +17,7 @@ open Environ
 (** printers *)
 val print_sort : sorts -> std_ppcmds
 val pr_sort_family : sorts_family -> std_ppcmds
-val pr_fix : (constr -> std_ppcmds) -> fixpoint -> 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
-- 
cgit v1.2.3


From b365304d32db443194b7eaadda63c784814f53f1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Nov 2016 03:23:13 +0100
Subject: Evarconv API using EConstr.

---
 engine/termops.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index b536b0fb8b..24c2c82f2f 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -254,6 +254,7 @@ val clear_named_body : Id.t -> env -> env
 
 val global_vars : env -> Evd.evar_map -> EConstr.t -> Id.t list
 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
 
 (** Gives an ordered list of hypotheses, closed by dependencies,
    containing a given set *)
-- 
cgit v1.2.3


From b77579ac873975a15978c5a4ecf312d577746d26 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Nov 2016 21:59:18 +0100
Subject: Tacred API using EConstr.

---
 engine/termops.mli | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 24c2c82f2f..4becca907c 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -65,9 +65,10 @@ 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 -> constr -> constr) ->
-    'a -> constr -> constr
+  ('a -> EConstr.constr -> EConstr.constr) ->
+    'a -> EConstr.constr -> EConstr.constr
 val map_constr_with_full_binders :
   Evd.evar_map ->
   (Context.Rel.Declaration.t -> 'a -> 'a) ->
-- 
cgit v1.2.3


From 3b8acc174490878a3d0c9345e34a0ecb1d3abd66 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 7 Nov 2016 13:27:16 +0100
Subject: Typeclasses API using EConstr.

---
 engine/termops.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 4becca907c..c90fdf9c2e 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -264,6 +264,8 @@ 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 isGlobalRef : Evd.evar_map -> EConstr.t -> bool
 
 val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool
-- 
cgit v1.2.3


From 67dc22d8389234d0c9b329944ff579e7056b7250 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 8 Nov 2016 10:57:05 +0100
Subject: Cases API using EConstr.

---
 engine/termops.mli | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index c90fdf9c2e..2b66c88a7f 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -45,11 +45,11 @@ 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 -> types -> types
+val mkProd_wo_LetIn : Context.Rel.Declaration.t -> EConstr.types -> EConstr.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 : 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 : types -> Context.Named.t -> types
 val it_mkNamedProd_wo_LetIn : types -> Context.Named.t -> types
@@ -170,6 +170,8 @@ val eta_reduce_head : constr -> constr
 (** Flattens application lists *)
 val collapse_appl : Evd.evar_map -> EConstr.t -> constr
 
+val prod_applist : Evd.evar_map -> EConstr.t -> EConstr.t list -> EConstr.t
+
 (** 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 -> constr
-- 
cgit v1.2.3


From c2855a3387be134d1220f301574b743572a94239 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 10 Nov 2016 11:39:27 +0100
Subject: Unification API using EConstr.

---
 engine/termops.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 2b66c88a7f..df3fdd124e 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -29,7 +29,7 @@ val print_rel_context : env -> std_ppcmds
 val print_env : env -> std_ppcmds
 
 (** about contexts *)
-val push_rel_assum : Name.t * types -> env -> env
+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
 
@@ -208,8 +208,8 @@ val decompose_app_vect : Evd.evar_map -> EConstr.t -> constr * 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)
+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)
 
 (** name contexts *)
 type names_context = Name.t list
-- 
cgit v1.2.3


From ca993b9e7765ac58f70740818758457c9367b0da Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 00:29:02 +0100
Subject: Making judgment type generic over the type of inner constrs.

This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.

Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
---
 engine/termops.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index df3fdd124e..27b3ea53ca 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -274,10 +274,10 @@ val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool
 
 (** Combinators on judgments *)
 
-val on_judgment       : (types -> types) -> unsafe_judgment -> unsafe_judgment
-val on_judgment_value : (types -> types) -> unsafe_judgment -> unsafe_judgment
-val on_judgment_type  : (types -> types) -> unsafe_judgment -> unsafe_judgment
+val on_judgment       : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
+val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
+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 coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set
+val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set
-- 
cgit v1.2.3


From 45562afa065aadc207dca4e904e309d835cb66ef Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 12 Nov 2016 01:28:45 +0100
Subject: Tacticals API using EConstr.

---
 engine/termops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 27b3ea53ca..02e8dfeaea 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -201,7 +201,7 @@ val nb_prod : Evd.evar_map -> EConstr.t -> int
 val nb_prod_modulo_zeta : Evd.evar_map -> EConstr.t -> int
 
 (** Get the last arg of a constr intended to be an application *)
-val last_arg : Evd.evar_map -> EConstr.t -> constr
+val last_arg : Evd.evar_map -> EConstr.t -> EConstr.constr
 
 (** Force the decomposition of a term as an applicative one *)
 val decompose_app_vect : Evd.evar_map -> EConstr.t -> constr * constr array
-- 
cgit v1.2.3


From 771be16883c8c47828f278ce49545716918764c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 12 Nov 2016 01:52:15 +0100
Subject: Hipattern API using EConstr.

---
 engine/termops.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 02e8dfeaea..abc9caa98e 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -268,6 +268,8 @@ val is_section_variable : Id.t -> bool
 
 val global_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses
 
+val is_global : Evd.evar_map -> Globnames.global_reference -> EConstr.constr -> bool
+
 val isGlobalRef : Evd.evar_map -> EConstr.t -> bool
 
 val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool
-- 
cgit v1.2.3


From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 13 Nov 2016 20:38:41 +0100
Subject: Tactics API using EConstr.

---
 engine/termops.mli | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index abc9caa98e..7758a57eee 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -41,7 +41,7 @@ val lookup_rel_id : Id.t -> Context.Rel.t -> int * constr option * types
     [rel_vect n m] builds [|Rel (n+m);...;Rel(n+1)|]
 *)
 val rel_vect : int -> int -> constr array
-val rel_list : int -> int -> constr list
+val rel_list : int -> int -> EConstr.constr list
 
 (** iterators/destructors on terms *)
 val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
@@ -160,10 +160,10 @@ val replace_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.t -> constr
 
 (** Alternative term equalities *)
 val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool
-val compare_constr_univ : (Reduction.conv_pb -> constr -> constr -> bool) ->
-  Reduction.conv_pb -> constr -> constr -> bool
-val constr_cmp : Reduction.conv_pb -> constr -> constr -> bool
-val eq_constr : constr -> constr -> bool (* FIXME rename: erases universes*)
+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 eta_reduce_head : constr -> constr
 
@@ -185,7 +185,7 @@ exception 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 : Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst
+val filtering : Evd.evar_map -> Context.Rel.t -> Reduction.conv_pb -> 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
-- 
cgit v1.2.3


From 3f9e56fcbf479999325a86bbdaeefd6a0be13c65 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Nov 2016 20:35:01 +0100
Subject: Equality API using EConstr.

---
 engine/termops.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 7758a57eee..013efcbcb3 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -256,6 +256,7 @@ 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_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
 
-- 
cgit v1.2.3


From db252cb87e9c63f400fd4fddd2d771df3160d592 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Nov 2016 01:07:35 +0100
Subject: Inv API using EConstr.

---
 engine/termops.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 013efcbcb3..1c14e6c897 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -46,8 +46,8 @@ val rel_list : int -> int -> EConstr.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 : types -> (Name.t * types) list -> types
-val it_mkLambda : constr -> (Name.t * types) list -> constr
+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 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
-- 
cgit v1.2.3


From 7b43de20a4acd7c9da290f038d9a16fe67eccd59 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Nov 2016 01:59:07 +0100
Subject: Leminv API using EConstr.

---
 engine/termops.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 1c14e6c897..72c0cedda3 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -51,9 +51,9 @@ val it_mkLambda : EConstr.constr -> (Name.t * EConstr.types) list -> EConstr.con
 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 : types -> Context.Named.t -> types
+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 : constr -> Context.Named.t -> constr
+val it_mkNamedLambda_or_LetIn : EConstr.constr -> Context.Named.t -> EConstr.constr
 
 (* Ad hoc version reinserting letin, assuming the body is defined in
    the context where the letins are expanded *)
-- 
cgit v1.2.3


From 34e86e839be251717db96f1f5969d7724ab43097 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Nov 2016 02:45:54 +0100
Subject: Hints API using EConstr.

---
 engine/termops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 72c0cedda3..a865c80fbb 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -96,7 +96,7 @@ val iter_constr_with_full_binders :
 (**********************************************************************)
 
 val strip_head_cast : Evd.evar_map -> EConstr.t -> EConstr.t
-val drop_extra_implicit_args : Evd.evar_map -> EConstr.t -> constr
+val drop_extra_implicit_args : Evd.evar_map -> EConstr.t -> EConstr.constr
 
 (** occur checks *)
 
-- 
cgit v1.2.3


From d833b81b49366e95cf20a1d00f9c63883adb8942 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 03:04:13 +0100
Subject: Rewrite API using EConstr.

---
 engine/termops.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index a865c80fbb..05604beda8 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -275,6 +275,8 @@ val isGlobalRef : Evd.evar_map -> EConstr.t -> bool
 
 val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool
 
+val is_Prop : Evd.evar_map -> EConstr.t -> bool
+
 (** Combinators on judgments *)
 
 val on_judgment       : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
-- 
cgit v1.2.3


From d4b344acb23f19b089098b7788f37ea22bc07b81 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 20:09:26 +0100
Subject: Eliminating parts of the right-hand side compatibility layer

---
 engine/termops.mli | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 05604beda8..426b5f34d8 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -144,7 +144,7 @@ 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 -> constr
+  (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> EConstr.t -> EConstr.t -> EConstr.constr
 
 (** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq]
    as equality *)
@@ -153,7 +153,7 @@ val replace_term_gen :
     EConstr.t -> EConstr.t -> EConstr.t -> constr
 
 (** [subst_term d c] replaces [d] by [Rel 1] in [c] *)
-val subst_term : Evd.evar_map -> EConstr.t -> EConstr.t -> constr
+val subst_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.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
@@ -174,7 +174,7 @@ val prod_applist : Evd.evar_map -> EConstr.t -> EConstr.t list -> EConstr.t
 
 (** 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 -> constr
+val strip_outer_cast : Evd.evar_map -> EConstr.t -> EConstr.constr
 
 exception CannotFilter
 
@@ -204,10 +204,10 @@ val nb_prod_modulo_zeta : Evd.evar_map -> EConstr.t -> int
 val last_arg : Evd.evar_map -> EConstr.t -> EConstr.constr
 
 (** Force the decomposition of a term as an applicative one *)
-val decompose_app_vect : Evd.evar_map -> EConstr.t -> constr * constr array
+val decompose_app_vect : Evd.evar_map -> EConstr.t -> 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_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)
 
-- 
cgit v1.2.3


From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Nov 2016 12:13:05 +0100
Subject: Reductionops now return EConstrs.

---
 engine/termops.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 426b5f34d8..1699d600e2 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -130,6 +130,7 @@ val occur_term : Evd.evar_map -> EConstr.t -> EConstr.t -> bool (** Synonymous o
 (* 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 assignment for metavariables *)
 type meta_type_map = (metavariable * types) list
-- 
cgit v1.2.3


From b36adb2124d3ba8a5547605e7f89bb0835d0ab10 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 15:50:17 +0100
Subject: Removing some return type compatibility layers in Termops.

---
 engine/termops.mli | 185 ++++++++++++++++++++++++++---------------------------
 1 file changed, 91 insertions(+), 94 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 1699d600e2..d7d9c743da 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
-- 
cgit v1.2.3


From 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 18:18:17 +0100
Subject: Ltac now uses evar-based constrs.

---
 engine/termops.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index d7d9c743da..3f924cfa14 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -21,9 +21,9 @@ 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.constr -> std_ppcmds) -> unit
-val print_constr     : Constr.constr -> std_ppcmds
-val print_constr_env : env -> Constr.constr -> std_ppcmds
+val set_print_constr : (env -> Evd.evar_map -> constr -> std_ppcmds) -> unit
+val print_constr     : constr -> std_ppcmds
+val print_constr_env : env -> Evd.evar_map -> 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
-- 
cgit v1.2.3


From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 02:12:40 +0100
Subject: Evar-normalizing functions now act on EConstrs.

---
 engine/termops.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 3f924cfa14..196962354c 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -12,8 +12,8 @@
 open Pp
 open Names
 open Term
-open EConstr
 open Environ
+open EConstr
 
 (** printers *)
 val print_sort : sorts -> std_ppcmds
@@ -283,4 +283,4 @@ val on_judgment_type  : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) puns
 
 (** {6 Functions to deal with impossible cases } *)
 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
+val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set
-- 
cgit v1.2.3


From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 16:18:47 +0100
Subject: 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.
---
 engine/termops.mli | 49 ++++++++++++++++++++++++++-----------------------
 1 file changed, 26 insertions(+), 23 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 196962354c..841de34b1e 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -34,7 +34,7 @@ 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.constr option * Constr.types
+val lookup_rel_id : Id.t -> ('c, 't) Context.Rel.pt -> int * 'c option * 't
 (** Associates the contents of an identifier in a [rel_context]. Raise
     [Not_found] if there is no such identifier. *)
 
@@ -45,16 +45,16 @@ 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 -> types -> types
+val mkProd_or_LetIn : rel_declaration -> types -> types
+val mkProd_wo_LetIn : rel_declaration -> 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 : types -> Context.Rel.t -> types
+val it_mkProd_or_LetIn : types -> rel_context -> types
+val it_mkProd_wo_LetIn : types -> rel_context -> 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_or_LetIn : types -> named_context -> types
 val it_mkNamedProd_wo_LetIn : Constr.types -> Context.Named.t -> Constr.types
-val it_mkNamedLambda_or_LetIn : constr -> Context.Named.t -> constr
+val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
 
 (* Ad hoc version reinserting letin, assuming the body is defined in
    the context where the letins are expanded *)
@@ -64,12 +64,12 @@ val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Context.Rel.t -> Const
 
 val map_constr_with_binders_left_to_right :
   Evd.evar_map ->
-  (Context.Rel.Declaration.t -> 'a -> 'a) ->
+  (rel_declaration -> 'a -> 'a) ->
   ('a -> constr -> constr) ->
     'a -> constr -> constr
 val map_constr_with_full_binders :
   Evd.evar_map ->
-  (Context.Rel.Declaration.t -> 'a -> 'a) ->
+  (rel_declaration -> 'a -> 'a) ->
   ('a -> constr -> constr) -> 'a -> constr -> constr
 
 (** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
@@ -105,7 +105,7 @@ 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
+  Id.t -> named_declaration -> bool
 
 (** As {!occur_var} but assume the identifier not to be a section variable *)
 val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool
@@ -117,7 +117,7 @@ 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 dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> 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 *)
@@ -182,11 +182,11 @@ 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.constr) Evar.Map.t
-val filtering : Evd.evar_map -> Context.Rel.t -> Reduction.conv_pb -> Constr.constr -> Constr.constr -> subst
+type subst = (rel_context * constr) Evar.Map.t
+val filtering : Evd.evar_map -> rel_context -> Reduction.conv_pb -> constr -> constr -> subst
 
-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
+val decompose_prod_letin : Evd.evar_map -> constr -> int * rel_context * constr
+val align_prod_letin : Evd.evar_map -> constr -> constr -> rel_context * constr
 
 (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction
    gives {% $ %}n{% $ %} (casts are ignored) *)
@@ -215,8 +215,8 @@ val add_name : Name.t -> names_context -> names_context
 val lookup_name_of_rel : int -> names_context -> Name.t
 val lookup_rel_of_name : Id.t -> names_context -> int
 val empty_names_context : names_context
-val ids_of_rel_context : Context.Rel.t -> Id.t list
-val ids_of_named_context : Context.Named.t -> Id.t list
+val ids_of_rel_context : ('c, 't) Context.Rel.pt -> Id.t list
+val ids_of_named_context : ('c, 't) Context.Named.pt -> Id.t list
 val ids_of_context : env -> Id.t list
 val names_of_rel_context : env -> names_context
 
@@ -228,15 +228,15 @@ val context_chop : int -> Context.Rel.t -> Context.Rel.t * Context.Rel.t
 (* [env_rel_context_chop n env] extracts out the [n] top declarations
    of the rel_context part of [env], counting both local definitions and
    hypotheses *)
-val env_rel_context_chop : int -> env -> env * Context.Rel.t
+val env_rel_context_chop : int -> env -> env * rel_context
 
 (** Set of local names *)
 val vars_of_env: env -> Id.Set.t
 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.constr) list
+val process_rel_context : (rel_declaration -> env -> env) -> env -> env
+val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Name.t * 't) list
 val lift_rel_context : int -> 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 *)
@@ -244,23 +244,26 @@ val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in contex
 val map_rel_context_in_env :
   (env -> Constr.constr -> Constr.constr) -> env -> Context.Rel.t -> Context.Rel.t
 val map_rel_context_with_binders :
-  (int -> Constr.constr -> Constr.constr) -> Context.Rel.t -> Context.Rel.t
+  (int -> 'c -> 'c) -> ('c, 'c) Context.Rel.pt -> ('c, 'c) Context.Rel.pt
 val fold_named_context_both_sides :
   ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) ->
     Context.Named.t -> init:'a -> 'a
 val mem_named_context_val : Id.t -> named_context_val -> bool
 val compact_named_context : Context.Named.t -> Context.Compacted.t
 
+val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt
+val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt
+
 val clear_named_body : Id.t -> env -> env
 
 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_vars_set_of_decl : env -> Evd.evar_map -> named_declaration -> Id.Set.t
 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 *)
-val dependency_closure : env -> Evd.evar_map -> Context.Named.t -> Id.Set.t -> Id.t list
+val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id.t list
 
 (** Test if an identifier is the basename of a global reference *)
 val is_section_variable : Id.t -> bool
-- 
cgit v1.2.3


From 27fbf069ccd846383bcfb35ba1ea5bd1d95090a0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Nov 2016 23:48:28 +0100
Subject: Moving printing code from Evd to Termops.

---
 engine/termops.mli | 36 +++++++++++++++++++++++++++---------
 1 file changed, 27 insertions(+), 9 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 841de34b1e..512bb05ff9 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -20,15 +20,6 @@ val print_sort : sorts -> std_ppcmds
 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 -> Evd.evar_map -> constr -> std_ppcmds) -> unit
-val print_constr     : constr -> std_ppcmds
-val print_constr_env : env -> Evd.evar_map -> 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 * types -> env -> env
 val push_rels_assum : (Name.t * Constr.types) list -> env -> env
@@ -287,3 +278,30 @@ val on_judgment_type  : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) puns
 (** {6 Functions to deal with impossible cases } *)
 val set_impossible_default_clause : (unit -> (Constr.constr * Constr.types) Univ.in_universe_context_set) -> unit
 val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set
+
+(** {5 Debug pretty-printers} *)
+
+open Evd
+
+val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
+
+val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
+
+val pr_evar_info : evar_info -> Pp.std_ppcmds
+val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds
+val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds
+val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) ->
+  evar_map -> Pp.std_ppcmds
+val pr_metaset : Metaset.t -> Pp.std_ppcmds
+val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds
+val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds
+
+(** debug printer: do not use to display terms to the casual user... *)
+
+val set_print_constr : (env -> Evd.evar_map -> constr -> std_ppcmds) -> unit
+val print_constr     : constr -> std_ppcmds
+val print_constr_env : env -> Evd.evar_map -> 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
-- 
cgit v1.2.3


From be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 30 Nov 2016 00:41:31 +0100
Subject: Namegen primitives now apply on evar constrs.

Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
---
 engine/termops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 512bb05ff9..0dd5d96fbd 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -288,7 +288,7 @@ val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
 val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
 
 val pr_evar_info : evar_info -> Pp.std_ppcmds
-val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds
+val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.std_ppcmds
 val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds
 val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) ->
   evar_map -> Pp.std_ppcmds
-- 
cgit v1.2.3


From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 1 Apr 2017 02:36:16 +0200
Subject: Using delayed universe instances in EConstr.

The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
---
 engine/termops.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/termops.mli')

diff --git a/engine/termops.mli b/engine/termops.mli
index 0dd5d96fbd..fe6dfb0ce1 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -250,7 +250,7 @@ val clear_named_body : Id.t -> env -> env
 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 -> named_declaration -> Id.Set.t
-val global_app_of_constr : Evd.evar_map -> constr -> Globnames.global_reference puniverses * constr option
+val global_app_of_constr : Evd.evar_map -> constr -> (Globnames.global_reference * EInstance.t) * constr option
 
 (** Gives an ordered list of hypotheses, closed by dependencies,
    containing a given set *)
@@ -259,7 +259,7 @@ val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id.
 (** 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 -> constr -> Globnames.global_reference puniverses
+val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference * EInstance.t
 
 val is_global : Evd.evar_map -> Globnames.global_reference -> constr -> bool
 
-- 
cgit v1.2.3