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.ml | 40 ++++++++++++++++++++--------------------
 1 file changed, 20 insertions(+), 20 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 9fa49264fe..55bf5f29ea 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -45,8 +45,8 @@ type debug = Debug | Info | Off
 
 exception Bound
 
-let head_constr_bound t =
-  let t = strip_outer_cast t in
+let head_constr_bound sigma t =
+  let t = strip_outer_cast sigma (EConstr.of_constr t) in
   let _,ccl = decompose_prod_assum t in
   let hd,args = decompose_app ccl in
   match kind_of_term hd with
@@ -54,13 +54,13 @@ let head_constr_bound t =
     | Proj (p, _) -> mkConst (Projection.constant p)
     | _ -> raise Bound
 
-let head_constr c =
-  try head_constr_bound c with Bound -> error "Bound head variable."
+let head_constr sigma c =
+  try head_constr_bound sigma c with Bound -> error "Bound head variable."
 
-let decompose_app_bound t =
-  let t = strip_outer_cast t in
+let decompose_app_bound sigma t =
+  let t = strip_outer_cast sigma (EConstr.of_constr t) in
   let _,ccl = decompose_prod_assum t in
-  let hd,args = decompose_app_vect ccl in
+  let hd,args = decompose_app_vect sigma (EConstr.of_constr ccl) in
   match kind_of_term hd with
     | Const (c,u) -> ConstRef c, args
     | Ind (i,u) -> IndRef i, args
@@ -505,7 +505,7 @@ struct
 
   let match_mode m arg =
     match m with
-    | ModeInput -> not (occur_existential arg)
+    | ModeInput -> not (occur_existential Evd.empty (EConstr.of_constr arg)) (** FIXME *)
     | ModeNoHeadEvar ->
        Evarutil.(try ignore(head_evar arg); false
                  with NoHeadEvar -> true)
@@ -742,7 +742,7 @@ let secvars_of_global env gr =
 
 let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
   let secvars = secvars_of_constr env c in
-  let cty = strip_outer_cast cty in
+  let cty = strip_outer_cast sigma (EConstr.of_constr cty) in
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
@@ -911,7 +911,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let c,ctx = fresh_global_or_constr env sigma poly r in
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
   let t = hnf_constr env sigma (unsafe_type_of env sigma c) in
-  let hd = head_of_constr_reference (head_constr t) in
+  let hd = head_of_constr_reference (head_constr sigma t) in
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
 	      poly = poly;
@@ -1013,7 +1013,7 @@ let subst_autohint (subst, obj) =
   let subst_key gr =
     let (lab'', elab') = subst_global subst gr in
     let gr' =
-      (try head_of_constr_reference (head_constr_bound elab')
+      (try head_of_constr_reference (head_constr_bound Evd.empty (** FIXME *) elab')
        with Bound -> lab'')
     in if gr' == gr then gr else gr'
   in
@@ -1190,17 +1190,17 @@ let prepare_hint check (poly,local) env init (sigma,c) =
      thing make_resolves will do is to re-instantiate the products *)
   let sigma, subst = Evd.nf_univ_variables sigma in
   let c = Vars.subst_univs_constr subst (Evarutil.nf_evar sigma c) in
-  let c = drop_extra_implicit_args c in
-  let vars = ref (collect_vars c) in
+  let c = drop_extra_implicit_args sigma (EConstr.of_constr c) in
+  let vars = ref (collect_vars sigma (EConstr.of_constr c)) in
   let subst = ref [] in
   let rec find_next_evar c = match kind_of_term c with
     | Evar (evk,args as ev) ->
       (* We skip the test whether args is the identity or not *)
       let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
-      let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in
+      let t = List.fold_right (fun (e,id) c -> replace_term sigma (EConstr.of_constr e) (EConstr.of_constr id) (EConstr.of_constr c)) !subst t in
       if not (closed0 c) then
 	error "Hints with holes dependent on a bound variable not supported.";
-      if occur_existential t then
+      if occur_existential sigma (EConstr.of_constr t) then
 	(* Not clever enough to construct dependency graph of evars *)
 	error "Not clever enough to deal with evars dependent in other evars.";
       raise (Found (c,t))
@@ -1211,7 +1211,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
       let id = next_ident_away_from default_prepare_hint_ident (fun id -> Id.Set.mem id !vars) in
       vars := Id.Set.add id !vars;
       subst := (evar,mkVar id)::!subst;
-      mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in
+      mkNamedLambda id t (iter (replace_term sigma (EConstr.of_constr evar) (EConstr.mkVar id) (EConstr.of_constr c))) in
   let c' = iter c in
     if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c';
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
@@ -1394,13 +1394,13 @@ let pr_hint_ref ref = pr_hint_list_for_head ref
 
 (* Print all hints associated to head id in any database *)
 
-let pr_hint_term cl =
+let pr_hint_term sigma cl =
   try
     let dbs = current_db () in
     let valid_dbs =
       let fn = try
-	  let hdc = decompose_app_bound cl in
-	    if occur_existential cl then
+	  let hdc = decompose_app_bound sigma cl in
+	    if occur_existential sigma (EConstr.of_constr cl) then
 	      Hint_db.map_existential ~secvars:Id.Pred.full hdc cl
 	    else Hint_db.map_auto ~secvars:Id.Pred.full hdc cl
 	with Bound -> Hint_db.map_none ~secvars:Id.Pred.full
@@ -1423,7 +1423,7 @@ let pr_applicable_hint () =
   match glss.Evd.it with
   | [] -> CErrors.error "No focused goal."
   | g::_ ->
-    pr_hint_term (Goal.V82.concl glss.Evd.sigma g)
+    pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g)
 
 let pp_hint_mode = function
   | ModeInput -> str"+"
-- 
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.

---
 tactics/hints.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 55bf5f29ea..c41f88ab7f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -761,7 +761,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
 	    code = with_uid (Give_exact (c, cty, ctx)); })
 
 let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
-  let cty = if hnf then hnf_constr env sigma cty else cty in
+  let cty = if hnf then hnf_constr env sigma (EConstr.of_constr cty) else cty in
     match kind_of_term cty with
     | Prod _ ->
         let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
@@ -910,7 +910,7 @@ let make_mode ref m =
 let make_trivial env sigma poly ?(name=PathAny) r =
   let c,ctx = fresh_global_or_constr env sigma poly r in
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
-  let t = hnf_constr env sigma (unsafe_type_of env sigma c) in
+  let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma c)) in
   let hd = head_of_constr_reference (head_constr sigma t) in
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
-- 
cgit v1.2.3


From d528fdaf12b74419c47698cca7c6f1ec762245a3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Nov 2016 14:48:36 +0100
Subject: Retyping API using EConstr.

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

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index c41f88ab7f..2aa4347779 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -846,7 +846,7 @@ let fresh_global_or_constr env sigma poly cr =
 
 let make_resolves env sigma flags pri poly ?name cr =
   let c, ctx = fresh_global_or_constr env sigma poly cr in
-  let cty = Retyping.get_type_of env sigma c in
+  let cty = Retyping.get_type_of env sigma (EConstr.of_constr c) in
   let try_apply f =
     try Some (f (c, cty, ctx)) with Failure _ -> None in
   let ents = List.map_filter try_apply
-- 
cgit v1.2.3


From e27949240f5b1ee212e7d0fe3326a21a13c4abb0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Nov 2016 17:21:44 +0100
Subject: Typing API using EConstr.

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

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2aa4347779..63d10573a9 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -910,7 +910,7 @@ let make_mode ref m =
 let make_trivial env sigma poly ?(name=PathAny) r =
   let c,ctx = fresh_global_or_constr env sigma poly r in
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
-  let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma c)) in
+  let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma (EConstr.of_constr c))) in
   let hd = head_of_constr_reference (head_constr sigma t) in
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
-- 
cgit v1.2.3


From 77e638121b6683047be915da9d0499a58fcb6e52 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Nov 2016 19:30:24 +0100
Subject: Patternops API using EConstr.

---
 tactics/hints.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 63d10573a9..b2aa02191e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -746,7 +746,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-	let pat = Patternops.pattern_of_constr env sigma cty in
+	let pat = Patternops.pattern_of_constr env sigma (EConstr.of_constr cty) in
 	let hd =
 	  try head_pattern_bound pat
 	  with BoundPattern -> failwith "make_exact_entry"
@@ -767,7 +767,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
         let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
         let ce = mk_clenv_from_env env sigma' None (c,cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
-	let pat = Patternops.pattern_of_constr env ce.evd c' in
+	let pat = Patternops.pattern_of_constr env ce.evd (EConstr.of_constr c') in
         let hd =
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in
@@ -911,11 +911,11 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let c,ctx = fresh_global_or_constr env sigma poly r in
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
   let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma (EConstr.of_constr c))) in
-  let hd = head_of_constr_reference (head_constr sigma t) in
+  let hd = head_of_constr_reference sigma (EConstr.of_constr (head_constr sigma t)) in
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
 	      poly = poly;
-              pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce));
+              pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.of_constr (clenv_type ce)));
 	      name = name;
               db = None;
               secvars = secvars_of_constr env c;
@@ -1013,7 +1013,7 @@ let subst_autohint (subst, obj) =
   let subst_key gr =
     let (lab'', elab') = subst_global subst gr in
     let gr' =
-      (try head_of_constr_reference (head_constr_bound Evd.empty (** FIXME *) elab')
+      (try head_of_constr_reference Evd.empty (EConstr.of_constr (head_constr_bound Evd.empty (** FIXME *) elab'))
        with Bound -> lab'')
     in if gr' == gr then gr else gr'
   in
-- 
cgit v1.2.3


From 85ab3e298aa1d7333787c1fa44d25df189ac255c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 8 Nov 2016 19:02:40 +0100
Subject: Pretyping API using EConstr.

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

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index b2aa02191e..e8225df2d0 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1213,7 +1213,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
       subst := (evar,mkVar id)::!subst;
       mkNamedLambda id t (iter (replace_term sigma (EConstr.of_constr evar) (EConstr.mkVar id) (EConstr.of_constr c))) in
   let c' = iter c in
-    if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c';
+    if check then Pretyping.check_evars (Global.env()) Evd.empty sigma (EConstr.of_constr c');
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     if poly then IsConstr (c', diff)
     else if local then IsConstr (c', diff)
-- 
cgit v1.2.3


From 7267dfafe9215c35275a39814c8af451961e997c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 17:48:47 +0100
Subject: Goal API using EConstr.

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

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index e8225df2d0..57358bb769 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1423,7 +1423,7 @@ let pr_applicable_hint () =
   match glss.Evd.it with
   | [] -> CErrors.error "No focused goal."
   | g::_ ->
-    pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g)
+    pr_hint_term glss.Evd.sigma (EConstr.Unsafe.to_constr (Goal.V82.concl glss.Evd.sigma g))
 
 let pp_hint_mode = function
   | ModeInput -> str"+"
-- 
cgit v1.2.3


From 0489e8b56d7e10f7111c0171960e25d32201b963 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 21:55:33 +0100
Subject: Clenv API using EConstr.

---
 tactics/hints.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 57358bb769..ea95fb1ade 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -276,9 +276,11 @@ let strip_params env c =
 let instantiate_hint env sigma p =
   let mk_clenv (c, cty, ctx) =
     let sigma = Evd.merge_context_set univ_flexible sigma ctx in
+    let c = EConstr.of_constr c in
+    let cty = EConstr.of_constr cty in
     let cl = mk_clenv_from_env env sigma None (c,cty) in 
       {cl with templval = 
-	  { cl.templval with rebus = strip_params env cl.templval.rebus };
+	  { cl.templval with rebus = EConstr.of_constr (strip_params env (EConstr.Unsafe.to_constr cl.templval.rebus)) };
 	env = empty_env}
   in
   let code = match p.code.obj with
@@ -765,9 +767,9 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
     match kind_of_term cty with
     | Prod _ ->
         let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
-        let ce = mk_clenv_from_env env sigma' None (c,cty) in
+        let ce = mk_clenv_from_env env sigma' None (EConstr.of_constr c,EConstr.of_constr cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
-	let pat = Patternops.pattern_of_constr env ce.evd (EConstr.of_constr c') in
+	let pat = Patternops.pattern_of_constr env ce.evd c' in
         let hd =
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in
@@ -912,10 +914,10 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
   let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma (EConstr.of_constr c))) in
   let hd = head_of_constr_reference sigma (EConstr.of_constr (head_constr sigma t)) in
-  let ce = mk_clenv_from_env env sigma None (c,t) in
+  let ce = mk_clenv_from_env env sigma None (EConstr.of_constr c,EConstr.of_constr t) in
   (Some hd, { pri=1;
 	      poly = poly;
-              pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.of_constr (clenv_type ce)));
+              pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce));
 	      name = name;
               db = None;
               secvars = secvars_of_constr env c;
-- 
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.

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

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index ea95fb1ade..560e7e43da 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1320,7 +1320,7 @@ let make_local_hint_db env sigma ts eapply lems =
   let map c =
     let sigma = Sigma.Unsafe.of_evar_map sigma in
     let Sigma (c, sigma, _) = c.delayed env sigma in
-    (Sigma.to_evar_map sigma, c)
+    (Sigma.to_evar_map sigma, EConstr.Unsafe.to_constr c)
   in
   let lems = List.map map lems in
   let sign = Environ.named_context env in
-- 
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.

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

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 560e7e43da..c31e863830 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -737,7 +737,7 @@ let secvars_of_idset s =
       else p) s Id.Pred.empty
 
 let secvars_of_constr env c =
-  secvars_of_idset (global_vars_set env c)
+  secvars_of_idset (Environ.global_vars_set env c)
 
 let secvars_of_global env gr =
   secvars_of_idset (vars_of_global_reference env gr)
-- 
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.ml | 173 ++++++++++++++++++++++++++++++-------------------------
 1 file changed, 96 insertions(+), 77 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index c31e863830..cd5fc79f5e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -6,12 +6,16 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+module CVars = Vars
+
 open Pp
 open Util
 open CErrors
 open Names
-open Vars
 open Term
+open Evd
+open EConstr
+open Vars
 open Environ
 open Mod_subst
 open Globnames
@@ -21,7 +25,6 @@ open Libnames
 open Smartlocate
 open Misctypes
 open Tactypes
-open Evd
 open Termops
 open Inductiveops
 open Typing
@@ -46,22 +49,29 @@ type debug = Debug | Info | Off
 exception Bound
 
 let head_constr_bound sigma t =
-  let t = strip_outer_cast sigma (EConstr.of_constr t) in
-  let _,ccl = decompose_prod_assum t in
-  let hd,args = decompose_app ccl in
-  match kind_of_term hd with
-    | Const _ | Ind _ | Construct _ | Var _ -> hd
-    | Proj (p, _) -> mkConst (Projection.constant p)
-    | _ -> raise Bound
+  let t = strip_outer_cast sigma t in
+  let t = EConstr.of_constr t in
+  let _,ccl = decompose_prod_assum sigma t in
+  let hd,args = decompose_app sigma ccl in
+  match EConstr.kind sigma hd with
+  | Const (c, _) -> ConstRef c
+  | Ind (i, _) -> IndRef i
+  | Construct (c, _) -> ConstructRef c
+  | Var id -> VarRef id
+  | Proj (p, _) -> ConstRef (Projection.constant p)
+  | _ -> raise Bound
 
 let head_constr sigma c =
   try head_constr_bound sigma c with Bound -> error "Bound head variable."
 
 let decompose_app_bound sigma t =
-  let t = strip_outer_cast sigma (EConstr.of_constr t) in
-  let _,ccl = decompose_prod_assum t in
-  let hd,args = decompose_app_vect sigma (EConstr.of_constr ccl) in
-  match kind_of_term hd with
+  let t = strip_outer_cast sigma t in
+  let t = EConstr.of_constr t in
+  let _,ccl = decompose_prod_assum sigma t in
+  let hd,args = decompose_app_vect sigma ccl in
+  let hd = EConstr.of_constr hd in
+  let args = Array.map EConstr.of_constr args in
+  match EConstr.kind sigma hd with
     | Const (c,u) -> ConstRef c, args
     | Ind (i,u) -> IndRef i, args
     | Construct (c,u) -> ConstructRef c, args
@@ -245,6 +255,7 @@ let rebuild_dn st se =
   { se with sentry_bnet = dn' }
 
 let lookup_tacs concl st se =
+  let concl = EConstr.Unsafe.to_constr concl in
   let l'  = Bounded_net.lookup st se.sentry_bnet concl in
   let sl' = List.stable_sort pri_order_int l' in
   List.merge pri_order_int se.sentry_nopat sl'
@@ -256,10 +267,10 @@ let is_transparent_gr (ids, csts) = function
   | ConstRef cst -> Cpred.mem cst csts
   | IndRef _ | ConstructRef _ -> false
 
-let strip_params env c = 
-  match kind_of_term c with
+let strip_params env sigma c = 
+  match EConstr.kind sigma c with
   | App (f, args) -> 
-    (match kind_of_term f with
+    (match EConstr.kind sigma f with
     | Const (p,_) ->
       let cb = lookup_constant p env in
 	(match cb.Declarations.const_proj with
@@ -276,11 +287,9 @@ let strip_params env c =
 let instantiate_hint env sigma p =
   let mk_clenv (c, cty, ctx) =
     let sigma = Evd.merge_context_set univ_flexible sigma ctx in
-    let c = EConstr.of_constr c in
-    let cty = EConstr.of_constr cty in
     let cl = mk_clenv_from_env env sigma None (c,cty) in 
       {cl with templval = 
-	  { cl.templval with rebus = EConstr.of_constr (strip_params env (EConstr.Unsafe.to_constr cl.templval.rebus)) };
+	  { cl.templval with rebus = strip_params env sigma cl.templval.rebus };
 	env = empty_env}
   in
   let code = match p.code.obj with
@@ -445,11 +454,11 @@ val empty : ?name:hint_db_name -> transparent_state -> bool -> t
 val find : global_reference -> t -> search_entry
 val map_none : secvars:Id.Pred.t -> t -> full_hint list
 val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list
-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
-val map_eauto : secvars:Id.Pred.t ->
+val map_eauto : evar_map -> secvars:Id.Pred.t ->
 		(global_reference * constr array) -> constr -> t -> full_hint list
-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
 val add_list : env -> evar_map -> hint_entry list -> t -> t
@@ -505,21 +514,21 @@ struct
       (** Warn about no longer typable hint? *)
       None
 
-  let match_mode m arg =
+  let match_mode sigma m arg =
     match m with
-    | ModeInput -> not (occur_existential Evd.empty (EConstr.of_constr arg)) (** FIXME *)
+    | ModeInput -> not (occur_existential sigma arg)
     | ModeNoHeadEvar ->
-       Evarutil.(try ignore(head_evar arg); false
+       Evarutil.(try ignore(head_evar sigma arg); false
                  with NoHeadEvar -> true)
     | ModeOutput -> true
                                
-  let matches_mode args mode =
+  let matches_mode sigma args mode =
     Array.length mode == Array.length args &&
-      Array.for_all2 match_mode mode args
+      Array.for_all2 (match_mode sigma) mode args
       
-  let matches_modes args modes =
+  let matches_modes sigma args modes =
     if List.is_empty modes then true
-    else List.exists (matches_mode args) modes
+    else List.exists (matches_mode sigma args) modes
 
   let merge_entry secvars db nopat pat =
     let h = List.sort pri_order_int (List.map snd db.hintdb_nopat) in
@@ -535,22 +544,22 @@ struct
     merge_entry secvars db se.sentry_nopat se.sentry_pat
 	
   (** Precondition: concl has no existentials *)
-  let map_auto ~secvars (k,args) concl db =
+  let map_auto sigma ~secvars (k,args) concl db =
     let se = find k db in
     let st = if db.use_dn then  (Some db.hintdb_state) else None in
     let pat = lookup_tacs concl st se in
     merge_entry secvars db [] pat
 
-  let map_existential ~secvars (k,args) concl db =
+  let map_existential sigma ~secvars (k,args) concl db =
     let se = find k db in
-      if matches_modes args se.sentry_mode then
+      if matches_modes sigma args se.sentry_mode then
         merge_entry secvars db se.sentry_nopat se.sentry_pat
       else merge_entry secvars db [] []
 
   (* [c] contains an existential *)
-  let map_eauto ~secvars (k,args) concl db =
+  let map_eauto sigma ~secvars (k,args) concl db =
     let se = find k db in
-      if matches_modes args se.sentry_mode then
+      if matches_modes sigma args se.sentry_mode then
         let st = if db.use_dn then Some db.hintdb_state else None in
         let pat = lookup_tacs concl st se in
         merge_entry secvars db [] pat
@@ -718,8 +727,8 @@ let _ = Summary.declare_summary "search"
 (*             Auxiliary functions to prepare AUTOHINT objects            *)
 (**************************************************************************)
 
-let rec nb_hyp c = match kind_of_term c with
-  | Prod(_,_,c2) -> if noccurn 1 c2 then 1+(nb_hyp c2) else nb_hyp c2
+let rec nb_hyp sigma c = match EConstr.kind sigma c with
+  | Prod(_,_,c2) -> if noccurn sigma 1 c2 then 1+(nb_hyp sigma c2) else nb_hyp sigma c2
   | _ -> 0
 
 (* adding and removing tactics in the search table *)
@@ -736,19 +745,20 @@ let secvars_of_idset s =
         Id.Pred.add id p
       else p) s Id.Pred.empty
 
-let secvars_of_constr env c =
-  secvars_of_idset (Environ.global_vars_set env c)
+let secvars_of_constr env sigma c =
+  secvars_of_idset (Termops.global_vars_set env sigma c)
 
 let secvars_of_global env gr =
   secvars_of_idset (vars_of_global_reference env gr)
 
 let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
-  let secvars = secvars_of_constr env c in
-  let cty = strip_outer_cast sigma (EConstr.of_constr cty) in
-    match kind_of_term cty with
+  let secvars = secvars_of_constr env sigma c in
+  let cty = strip_outer_cast sigma cty in
+  let cty = EConstr.of_constr cty in
+    match EConstr.kind sigma cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-	let pat = Patternops.pattern_of_constr env sigma (EConstr.of_constr cty) in
+	let pat = Patternops.pattern_of_constr env sigma cty in
 	let hd =
 	  try head_pattern_bound pat
 	  with BoundPattern -> failwith "make_exact_entry"
@@ -763,21 +773,21 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
 	    code = with_uid (Give_exact (c, cty, ctx)); })
 
 let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
-  let cty = if hnf then hnf_constr env sigma (EConstr.of_constr cty) else cty in
-    match kind_of_term cty with
+  let cty = if hnf then EConstr.of_constr (hnf_constr env sigma cty) else cty in
+    match EConstr.kind sigma cty with
     | Prod _ ->
         let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
-        let ce = mk_clenv_from_env env sigma' None (EConstr.of_constr c,EConstr.of_constr cty) in
+        let ce = mk_clenv_from_env env sigma' None (c,cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
 	let pat = Patternops.pattern_of_constr env ce.evd c' in
         let hd =
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in
         let nmiss = List.length (clenv_missing ce) in
-        let secvars = secvars_of_constr env c in
+        let secvars = secvars_of_constr env sigma c in
 	if Int.equal nmiss 0 then
 	  (Some hd,
-          { pri = (match pri with None -> nb_hyp cty | Some p -> p);
+          { pri = (match pri with None -> nb_hyp sigma' cty | Some p -> p);
 	    poly = poly;
             pat = Some pat;
 	    name = name;
@@ -787,10 +797,10 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	else begin
 	  if not eapply then failwith "make_apply_entry";
           if verbose then
-	    Feedback.msg_info (str "the hint: eapply " ++ pr_lconstr c ++
+	    Feedback.msg_info (str "the hint: eapply " ++ pr_lconstr (EConstr.Unsafe.to_constr c) ++
 	    str " will only be used by eauto");
           (Some hd,
-           { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p);
+           { pri = (match pri with None -> nb_hyp sigma' cty + nmiss | Some p -> p);
 	     poly = poly;
              pat = Some pat;
 	     name = name;
@@ -808,7 +818,7 @@ let pr_hint_term env sigma ctx = function
   | IsGlobRef gr -> pr_global gr
   | IsConstr (c, ctx) ->
      let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
-     pr_constr_env env sigma c
+     pr_constr_env env sigma (EConstr.Unsafe.to_constr c)
 
 (** We need an object to record the side-effect of registering
   global universes associated with a hint. *)
@@ -834,7 +844,8 @@ let fresh_global_or_constr env sigma poly cr =
   let isgr, (c, ctx) =
     match cr with
     | IsGlobRef gr ->
-       true, Universes.fresh_global_instance env gr
+      let (c, ctx) = Universes.fresh_global_instance env gr in
+       true, (EConstr.of_constr c, ctx)
     | IsConstr (c, ctx) -> false, (c, ctx)
   in
     if poly then (c, ctx)
@@ -848,7 +859,8 @@ let fresh_global_or_constr env sigma poly cr =
 
 let make_resolves env sigma flags pri poly ?name cr =
   let c, ctx = fresh_global_or_constr env sigma poly cr in
-  let cty = Retyping.get_type_of env sigma (EConstr.of_constr c) in
+  let cty = Retyping.get_type_of env sigma c in
+  let cty = EConstr.of_constr cty in
   let try_apply f =
     try Some (f (c, cty, ctx)) with Failure _ -> None in
   let ents = List.map_filter try_apply
@@ -857,7 +869,7 @@ let make_resolves env sigma flags pri poly ?name cr =
   in
   if List.is_empty ents then
     user_err ~hdr:"Hint"
-      (pr_lconstr c ++ spc() ++
+      (pr_lconstr (EConstr.Unsafe.to_constr c) ++ spc() ++
         (if pi1 flags then str"cannot be used as a hint."
 	else str "can be used as a hint only for eauto."));
   ents
@@ -869,7 +881,7 @@ let make_resolve_hyp env sigma decl =
   try
     [make_apply_entry env sigma (true, true, false) None false
        ~name:(PathHints [VarRef hname])
-       (c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
+       (c, EConstr.of_constr (NamedDecl.get_type decl), Univ.ContextSet.empty)]
   with
     | Failure _ -> []
     | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp")
@@ -899,6 +911,7 @@ let make_extern pri pat tacast =
      code = with_uid (Extern tacast) })  
 
 let make_mode ref m = 
+  let open Term in
   let ty = Global.type_of_global_unsafe ref in
   let ctx, t = decompose_prod ty in
   let n = List.length ctx in
@@ -912,15 +925,16 @@ let make_mode ref m =
 let make_trivial env sigma poly ?(name=PathAny) r =
   let c,ctx = fresh_global_or_constr env sigma poly r in
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
-  let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma (EConstr.of_constr c))) in
-  let hd = head_of_constr_reference sigma (EConstr.of_constr (head_constr sigma t)) in
-  let ce = mk_clenv_from_env env sigma None (EConstr.of_constr c,EConstr.of_constr t) in
+  let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma c)) in
+  let t = EConstr.of_constr t in
+  let hd = head_constr sigma t in
+  let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
 	      poly = poly;
               pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce));
 	      name = name;
               db = None;
-              secvars = secvars_of_constr env c;
+              secvars = secvars_of_constr env sigma c;
               code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
 
 
@@ -1014,14 +1028,16 @@ let cache_autohint (kn, obj) =
 let subst_autohint (subst, obj) =
   let subst_key gr =
     let (lab'', elab') = subst_global subst gr in
+    let elab' = EConstr.of_constr elab' in
     let gr' =
-      (try head_of_constr_reference Evd.empty (EConstr.of_constr (head_constr_bound Evd.empty (** FIXME *) elab'))
+      (try head_constr_bound Evd.empty elab'
        with Bound -> lab'')
     in if gr' == gr then gr else gr'
   in
   let subst_hint (k,data as hint) =
     let k' = Option.smartmap subst_key k in
     let pat' = Option.smartmap (subst_pattern subst) data.pat in
+    let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
     let code' = match data.code.obj with
       | Res_pf (c,t,ctx) ->
           let c' = subst_mps subst c in
@@ -1191,31 +1207,33 @@ let prepare_hint check (poly,local) env init (sigma,c) =
      It is actually a bit stupid to generalize over evars since the first
      thing make_resolves will do is to re-instantiate the products *)
   let sigma, subst = Evd.nf_univ_variables sigma in
-  let c = Vars.subst_univs_constr subst (Evarutil.nf_evar sigma c) in
-  let c = drop_extra_implicit_args sigma (EConstr.of_constr c) in
-  let vars = ref (collect_vars sigma (EConstr.of_constr c)) in
+  let c = Evarutil.nf_evar sigma (EConstr.Unsafe.to_constr c) in
+  let c = CVars.subst_univs_constr subst c in
+  let c = EConstr.of_constr c in
+  let c = drop_extra_implicit_args sigma c in
+  let vars = ref (collect_vars sigma c) in
   let subst = ref [] in
-  let rec find_next_evar c = match kind_of_term c with
+  let rec find_next_evar c = match EConstr.kind sigma c with
     | Evar (evk,args as ev) ->
       (* We skip the test whether args is the identity or not *)
-      let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
-      let t = List.fold_right (fun (e,id) c -> replace_term sigma (EConstr.of_constr e) (EConstr.of_constr id) (EConstr.of_constr c)) !subst t in
-      if not (closed0 c) then
+      let t = existential_type sigma ev in
+      let t = List.fold_right (fun (e,id) c -> EConstr.of_constr (replace_term sigma e id c)) !subst t in
+      if not (closed0 sigma c) then
 	error "Hints with holes dependent on a bound variable not supported.";
-      if occur_existential sigma (EConstr.of_constr t) then
+      if occur_existential sigma t then
 	(* Not clever enough to construct dependency graph of evars *)
 	error "Not clever enough to deal with evars dependent in other evars.";
       raise (Found (c,t))
-    | _ -> Constr.iter find_next_evar c in
+    | _ -> EConstr.iter sigma find_next_evar c in
   let rec iter c =
     try find_next_evar c; c
     with Found (evar,t) ->
       let id = next_ident_away_from default_prepare_hint_ident (fun id -> Id.Set.mem id !vars) in
       vars := Id.Set.add id !vars;
       subst := (evar,mkVar id)::!subst;
-      mkNamedLambda id t (iter (replace_term sigma (EConstr.of_constr evar) (EConstr.mkVar id) (EConstr.of_constr c))) in
+      mkNamedLambda id t (iter (EConstr.of_constr (replace_term sigma evar (mkVar id) c))) in
   let c' = iter c in
-    if check then Pretyping.check_evars (Global.env()) Evd.empty sigma (EConstr.of_constr c');
+    if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c';
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     if poly then IsConstr (c', diff)
     else if local then IsConstr (c', diff)
@@ -1228,6 +1246,7 @@ let interp_hints poly =
   let sigma = Evd.from_env env in
   let f poly c =
     let evd,c = Constrintern.interp_open_constr env sigma c in
+    let c = EConstr.of_constr c in
       prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in
   let fref r =
     let gr = global_with_alias r in
@@ -1293,7 +1312,7 @@ let add_hints local dbnames0 h =
 
 let expand_constructor_hints env sigma lems =
   List.map_append (fun (evd,lem) ->
-    match kind_of_term lem with
+    match EConstr.kind sigma lem with
     | Ind (ind,u) ->
 	List.init (nconstructors ind) 
 		  (fun i ->
@@ -1320,7 +1339,7 @@ let make_local_hint_db env sigma ts eapply lems =
   let map c =
     let sigma = Sigma.Unsafe.of_evar_map sigma in
     let Sigma (c, sigma, _) = c.delayed env sigma in
-    (Sigma.to_evar_map sigma, EConstr.Unsafe.to_constr c)
+    (Sigma.to_evar_map sigma, c)
   in
   let lems = List.map map lems in
   let sign = Environ.named_context env in
@@ -1348,7 +1367,7 @@ let make_db_list dbnames =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
-let pr_hint_elt (c, _, _) = pr_constr c
+let pr_hint_elt (c, _, _) = pr_constr (EConstr.Unsafe.to_constr c)
 
 let pr_hint h = match h.obj with
   | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt c)
@@ -1402,9 +1421,9 @@ let pr_hint_term sigma cl =
     let valid_dbs =
       let fn = try
 	  let hdc = decompose_app_bound sigma cl in
-	    if occur_existential sigma (EConstr.of_constr cl) then
-	      Hint_db.map_existential ~secvars:Id.Pred.full hdc cl
-	    else Hint_db.map_auto ~secvars:Id.Pred.full hdc cl
+	    if occur_existential sigma cl then
+	      Hint_db.map_existential sigma ~secvars:Id.Pred.full hdc cl
+	    else Hint_db.map_auto sigma ~secvars:Id.Pred.full hdc cl
 	with Bound -> Hint_db.map_none ~secvars:Id.Pred.full
       in
       let fn db = List.map (fun x -> 0, x) (fn db) in
@@ -1425,7 +1444,7 @@ let pr_applicable_hint () =
   match glss.Evd.it with
   | [] -> CErrors.error "No focused goal."
   | g::_ ->
-    pr_hint_term glss.Evd.sigma (EConstr.Unsafe.to_constr (Goal.V82.concl glss.Evd.sigma g))
+    pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g)
 
 let pp_hint_mode = function
   | ModeInput -> str"+"
-- 
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

---
 tactics/hints.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index cd5fc79f5e..2b310033c3 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -50,7 +50,6 @@ exception Bound
 
 let head_constr_bound sigma t =
   let t = strip_outer_cast sigma t in
-  let t = EConstr.of_constr t in
   let _,ccl = decompose_prod_assum sigma t in
   let hd,args = decompose_app sigma ccl in
   match EConstr.kind sigma hd with
@@ -66,11 +65,8 @@ let head_constr sigma c =
 
 let decompose_app_bound sigma t =
   let t = strip_outer_cast sigma t in
-  let t = EConstr.of_constr t in
   let _,ccl = decompose_prod_assum sigma t in
   let hd,args = decompose_app_vect sigma ccl in
-  let hd = EConstr.of_constr hd in
-  let args = Array.map EConstr.of_constr args in
   match EConstr.kind sigma hd with
     | Const (c,u) -> ConstRef c, args
     | Ind (i,u) -> IndRef i, args
@@ -754,7 +750,6 @@ let secvars_of_global env gr =
 let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
   let secvars = secvars_of_constr env sigma c in
   let cty = strip_outer_cast sigma cty in
-  let cty = EConstr.of_constr cty in
     match EConstr.kind sigma cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-- 
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.

---
 tactics/hints.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2b310033c3..231695c35a 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -768,7 +768,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
 	    code = with_uid (Give_exact (c, cty, ctx)); })
 
 let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
-  let cty = if hnf then EConstr.of_constr (hnf_constr env sigma cty) else cty in
+  let cty = if hnf then hnf_constr env sigma cty else cty in
     match EConstr.kind sigma cty with
     | Prod _ ->
         let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
@@ -921,7 +921,6 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let c,ctx = fresh_global_or_constr env sigma poly r in
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
   let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma c)) in
-  let t = EConstr.of_constr t in
   let hd = head_constr sigma t in
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
-- 
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.

---
 tactics/hints.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 231695c35a..d4b73706ce 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1211,7 +1211,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
     | Evar (evk,args as ev) ->
       (* We skip the test whether args is the identity or not *)
       let t = existential_type sigma ev in
-      let t = List.fold_right (fun (e,id) c -> EConstr.of_constr (replace_term sigma e id c)) !subst t in
+      let t = List.fold_right (fun (e,id) c -> replace_term sigma e id c) !subst t in
       if not (closed0 sigma c) then
 	error "Hints with holes dependent on a bound variable not supported.";
       if occur_existential sigma t then
@@ -1225,7 +1225,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
       let id = next_ident_away_from default_prepare_hint_ident (fun id -> Id.Set.mem id !vars) in
       vars := Id.Set.add id !vars;
       subst := (evar,mkVar id)::!subst;
-      mkNamedLambda id t (iter (EConstr.of_constr (replace_term sigma evar (mkVar id) c))) in
+      mkNamedLambda id t (iter (replace_term sigma evar (mkVar id) c)) in
   let c' = iter c in
     if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c';
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
-- 
cgit v1.2.3


From 531590c223af42c07a93142ab0cea470a98964e6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 17:15:15 +0100
Subject: Removing compatibility layers in Retyping

---
 tactics/hints.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index d4b73706ce..9e9635e8ab 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -855,7 +855,6 @@ let fresh_global_or_constr env sigma poly cr =
 let make_resolves env sigma flags pri poly ?name cr =
   let c, ctx = fresh_global_or_constr env sigma poly cr in
   let cty = Retyping.get_type_of env sigma c in
-  let cty = EConstr.of_constr cty in
   let try_apply f =
     try Some (f (c, cty, ctx)) with Failure _ -> None in
   let ents = List.map_filter try_apply
-- 
cgit v1.2.3


From 778e863b77bcafc8ed339dd02226e85e5fee2532 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Nov 2016 11:36:09 +0100
Subject: Removing compatibility layers related to printing.

---
 tactics/hints.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 9e9635e8ab..2446b6996b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -792,7 +792,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	else begin
 	  if not eapply then failwith "make_apply_entry";
           if verbose then
-	    Feedback.msg_info (str "the hint: eapply " ++ pr_lconstr (EConstr.Unsafe.to_constr c) ++
+	    Feedback.msg_info (str "the hint: eapply " ++ pr_leconstr_env env sigma' c ++
 	    str " will only be used by eauto");
           (Some hd,
            { pri = (match pri with None -> nb_hyp sigma' cty + nmiss | Some p -> p);
@@ -813,7 +813,7 @@ let pr_hint_term env sigma ctx = function
   | IsGlobRef gr -> pr_global gr
   | IsConstr (c, ctx) ->
      let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
-     pr_constr_env env sigma (EConstr.Unsafe.to_constr c)
+     pr_econstr_env env sigma c
 
 (** We need an object to record the side-effect of registering
   global universes associated with a hint. *)
@@ -863,7 +863,7 @@ let make_resolves env sigma flags pri poly ?name cr =
   in
   if List.is_empty ents then
     user_err ~hdr:"Hint"
-      (pr_lconstr (EConstr.Unsafe.to_constr c) ++ spc() ++
+      (pr_leconstr_env env sigma c ++ spc() ++
         (if pi1 flags then str"cannot be used as a hint."
 	else str "can be used as a hint only for eauto."));
   ents
@@ -1360,7 +1360,7 @@ let make_db_list dbnames =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
-let pr_hint_elt (c, _, _) = pr_constr (EConstr.Unsafe.to_constr c)
+let pr_hint_elt (c, _, _) = pr_econstr c
 
 let pr_hint h = match h.obj with
   | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt c)
-- 
cgit v1.2.3


From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Nov 2016 18:34:53 +0100
Subject: Removing various compatibility layers of tactics.

---
 tactics/hints.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2446b6996b..851e9f01fb 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -919,7 +919,7 @@ let make_mode ref m =
 let make_trivial env sigma poly ?(name=PathAny) r =
   let c,ctx = fresh_global_or_constr env sigma poly r in
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
-  let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma c)) in
+  let t = hnf_constr env sigma (unsafe_type_of env sigma c) in
   let hd = head_constr sigma t in
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
@@ -1239,7 +1239,6 @@ let interp_hints poly =
   let sigma = Evd.from_env env in
   let f poly c =
     let evd,c = Constrintern.interp_open_constr env sigma c in
-    let c = EConstr.of_constr c in
       prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in
   let fref r =
     let gr = global_with_alias r in
-- 
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.

---
 tactics/hints.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 851e9f01fb..ef97b0b330 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1200,7 +1200,8 @@ let prepare_hint check (poly,local) env init (sigma,c) =
      It is actually a bit stupid to generalize over evars since the first
      thing make_resolves will do is to re-instantiate the products *)
   let sigma, subst = Evd.nf_univ_variables sigma in
-  let c = Evarutil.nf_evar sigma (EConstr.Unsafe.to_constr c) in
+  let c = Evarutil.nf_evar sigma c in
+  let c = EConstr.Unsafe.to_constr c in
   let c = CVars.subst_univs_constr subst c in
   let c = EConstr.of_constr c in
   let c = drop_extra_implicit_args sigma c in
-- 
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.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index ef97b0b330..ffd19ac6e0 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -875,7 +875,7 @@ let make_resolve_hyp env sigma decl =
   try
     [make_apply_entry env sigma (true, true, false) None false
        ~name:(PathHints [VarRef hname])
-       (c, EConstr.of_constr (NamedDecl.get_type decl), Univ.ContextSet.empty)]
+       (c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
   with
     | Failure _ -> []
     | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp")
@@ -1335,7 +1335,7 @@ let make_local_hint_db env sigma ts eapply lems =
     (Sigma.to_evar_map sigma, c)
   in
   let lems = List.map map lems in
-  let sign = Environ.named_context env in
+  let sign = EConstr.named_context env in
   let ts = match ts with
     | None -> Hint_db.transparent_state (searchtable_map "core") 
     | Some ts -> ts
-- 
cgit v1.2.3


From 390fd4ac0a969103caeb5db3e5138e26f9a533de Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Nov 2016 17:49:11 +0100
Subject: Chasing a few unsafe constr coercions.

---
 tactics/hints.ml | 20 +++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index ffd19ac6e0..17c81064d7 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -250,9 +250,8 @@ let rebuild_dn st se =
   in
   { se with sentry_bnet = dn' }
 
-let lookup_tacs concl st se =
-  let concl = EConstr.Unsafe.to_constr concl in
-  let l'  = Bounded_net.lookup st se.sentry_bnet concl in
+let lookup_tacs sigma concl st se =
+  let l'  = Bounded_net.lookup sigma st se.sentry_bnet concl in
   let sl' = List.stable_sort pri_order_int l' in
   List.merge pri_order_int se.sentry_nopat sl'
 
@@ -510,6 +509,17 @@ struct
       (** Warn about no longer typable hint? *)
       None
 
+  let head_evar sigma c =
+    let rec hrec c = match EConstr.kind sigma c with
+      | Evar (evk,_)   -> evk
+      | Case (_,_,c,_) -> hrec c
+      | App (c,_)      -> hrec c
+      | Cast (c,_,_)   -> hrec c
+      | Proj (p, c)    -> hrec c
+      | _              -> raise Evarutil.NoHeadEvar
+    in
+    hrec c
+
   let match_mode sigma m arg =
     match m with
     | ModeInput -> not (occur_existential sigma arg)
@@ -543,7 +553,7 @@ struct
   let map_auto sigma ~secvars (k,args) concl db =
     let se = find k db in
     let st = if db.use_dn then  (Some db.hintdb_state) else None in
-    let pat = lookup_tacs concl st se in
+    let pat = lookup_tacs sigma concl st se in
     merge_entry secvars db [] pat
 
   let map_existential sigma ~secvars (k,args) concl db =
@@ -557,7 +567,7 @@ struct
     let se = find k db in
       if matches_modes sigma args se.sentry_mode then
         let st = if db.use_dn then Some db.hintdb_state else None in
-        let pat = lookup_tacs concl st se in
+        let pat = lookup_tacs sigma concl st se in
         merge_entry secvars db [] pat
       else merge_entry secvars db [] []
 
-- 
cgit v1.2.3


From 594ac9654164e377e8598894019cc4445509d570 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 17 Dec 2016 18:36:59 +0100
Subject: Removing a subtle nf_enter in Class_tactics.

The underlying hint mode implementation was not using the evar-insensitive
API so that it resulted in strange bugs.
---
 tactics/hints.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 17c81064d7..5aacafd6fa 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -524,8 +524,8 @@ struct
     match m with
     | ModeInput -> not (occur_existential sigma arg)
     | ModeNoHeadEvar ->
-       Evarutil.(try ignore(head_evar sigma arg); false
-                 with NoHeadEvar -> true)
+       (try ignore(head_evar sigma arg); false
+                 with Evarutil.NoHeadEvar -> true)
     | ModeOutput -> true
                                
   let matches_mode sigma args mode =
-- 
cgit v1.2.3


From 5db9588098f9f02d923c21f3914e3c671b10728f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 24 Jan 2017 13:07:11 +0100
Subject: Quick hack to fix interpretation of patterns in Ltac.

Interpretation of patterns in Ltac is essentially flawed. It does a roundtrip
through the pretyper, and relies on suspicious flagging of evars in the evar source
field to recognize original pattern holes. After the pattern_of_constr function
was made evar-insensitive, it expanded evars that were solved by magical side-effects
of the pretyper, even if it hadn't been asked to perform any heuristics.

We backtrack on the insensitivity of the pattern_of_constr function. This may have
a performance penalty in other dubious code, e.g. hints. In the long run we should
get rid of the pattern_of_constr function.
---
 tactics/hints.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 5aacafd6fa..a1c99c341e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -763,7 +763,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
     match EConstr.kind sigma cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-	let pat = Patternops.pattern_of_constr env sigma cty in
+	let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr sigma cty) in
 	let hd =
 	  try head_pattern_bound pat
 	  with BoundPattern -> failwith "make_exact_entry"
@@ -784,7 +784,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
         let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
         let ce = mk_clenv_from_env env sigma' None (c,cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
-	let pat = Patternops.pattern_of_constr env ce.evd c' in
+	let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma c') in
         let hd =
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in
@@ -934,7 +934,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
 	      poly = poly;
-              pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce));
+              pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce)));
 	      name = name;
               db = None;
               secvars = secvars_of_constr env sigma c;
-- 
cgit v1.2.3