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.

---
 tactics/hints.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/hints.mli')

diff --git a/tactics/hints.mli b/tactics/hints.mli
index edc65c4070..c0eb2c3b86 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -24,7 +24,7 @@ open Vernacexpr
 
 exception Bound
 
-val decompose_app_bound : constr -> global_reference * constr array
+val decompose_app_bound : evar_map -> constr -> global_reference * constr array
 
 type debug = Debug | Info | Off
 
-- 
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.

---
 tactics/hints.mli | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'tactics/hints.mli')

diff --git a/tactics/hints.mli b/tactics/hints.mli
index c0eb2c3b86..344827e03e 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -10,6 +10,7 @@ open Pp
 open Util
 open Names
 open Term
+open EConstr
 open Environ
 open Globnames
 open Decl_kinds
@@ -99,16 +100,16 @@ module Hint_db :
 
     (** All hints associated to the reference, respecting modes if evars appear in the 
 	arguments, _not_ using the discrimination net. *)
-    val map_existential : secvars:Id.Pred.t ->
+    val map_existential : evar_map -> secvars:Id.Pred.t ->
       (global_reference * constr array) -> constr -> t -> full_hint list
 
     (** All hints associated to the reference, respecting modes if evars appear in the 
 	arguments and using the discrimination net. *)
-    val map_eauto : secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list
+    val map_eauto : evar_map -> secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list
 
     (** All hints associated to the reference, respecting modes if evars appear in the 
 	arguments. *)
-    val map_auto : secvars:Id.Pred.t ->
+    val map_auto : evar_map -> secvars:Id.Pred.t ->
        (global_reference * constr array) -> constr -> t -> full_hint list
 
     val add_one : env -> evar_map -> hint_entry -> t -> t
@@ -170,7 +171,7 @@ val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
 
 val prepare_hint : bool (* Check no remaining evars *) ->
   (bool * bool) (* polymorphic or monomorphic, local or global *) ->
-  env -> evar_map -> open_constr -> hint_term
+  env -> evar_map -> evar_map * constr -> hint_term
 
 (** [make_exact_entry pri (c, ctyp, ctx, secvars)].
    [c] is the term given as an exact proof to solve the goal;
-- 
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.
---
 tactics/hints.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics/hints.mli')

diff --git a/tactics/hints.mli b/tactics/hints.mli
index 344827e03e..0d6dd434e9 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -29,7 +29,7 @@ val decompose_app_bound : evar_map -> constr -> global_reference * constr array
 
 type debug = Debug | Info | Off
 
-val secvars_of_hyps : Context.Named.t -> Id.Pred.t
+val secvars_of_hyps : ('c, 't) Context.Named.pt -> Id.Pred.t
 
 (** Pre-created hint databases *)
 
@@ -209,7 +209,7 @@ val make_resolves :
    If the hyp cannot be used as a Hint, the empty list is returned. *)
 
 val make_resolve_hyp :
-  env -> evar_map -> Context.Named.Declaration.t -> hint_entry list
+  env -> evar_map -> named_declaration -> hint_entry list
 
 (** [make_extern pri pattern tactic_expr] *)
 
-- 
cgit v1.2.3