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/eauto.ml | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'tactics/eauto.ml')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 10c975b8d8..6250fef2d6 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -32,7 +32,8 @@ let e_give_exact ?(flags=eauto_unif_flags) c =
   Proofview.Goal.enter { enter = begin fun gl ->
   let t1 = Tacmach.New.pf_unsafe_type_of gl c in
   let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
-  if occur_existential t1 || occur_existential t2 then
+  let sigma = Tacmach.New.project gl in
+  if occur_existential sigma (EConstr.of_constr t1) || occur_existential sigma (EConstr.of_constr t2) then
      Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
   else exact_check c
   end }
@@ -123,7 +124,7 @@ let hintmap_of secvars hdc concl =
   match hdc with
   | None -> fun db -> Hint_db.map_none ~secvars db
   | Some hdc ->
-     if occur_existential concl then
+     if occur_existential Evd.empty (EConstr.of_constr concl) then (** FIXME *)
        (fun db -> Hint_db.map_existential ~secvars hdc concl db)
      else (fun db -> Hint_db.map_auto ~secvars hdc concl db)
    (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
@@ -147,7 +148,7 @@ let rec e_trivial_fail_db db_list local_db =
   let tacl =
     registered_e_assumption ::
     (Tacticals.New.tclTHEN Tactics.intro next) ::
-    (List.map fst (e_trivial_resolve db_list local_db secvars (Tacmach.New.pf_nf_concl gl)))
+    (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_nf_concl gl)))
   in
   Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
   end }
@@ -181,13 +182,13 @@ and e_my_find_search db_list local_db secvars hdc concl =
   in
   List.map tac_of_hint hintl
 
-and e_trivial_resolve db_list local_db secvars gl =
-  let hd = try Some (decompose_app_bound gl) with Bound -> None in
+and e_trivial_resolve sigma db_list local_db secvars gl =
+  let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in
   try priority (e_my_find_search db_list local_db secvars hd gl)
   with Not_found -> []
 
-let e_possible_resolve db_list local_db secvars gl =
-  let hd = try Some (decompose_app_bound gl) with Bound -> None in
+let e_possible_resolve sigma db_list local_db secvars gl =
+  let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in
   try List.map (fun (b, (tac, pp)) -> (tac, b, pp))
                (e_my_find_search db_list local_db secvars hd gl)
   with Not_found -> []
@@ -289,7 +290,7 @@ module SearchProblem = struct
 	let l =
           let concl = Reductionops.nf_evar (project g)(pf_concl g) in
 	  filter_tactics s.tacres
-                         (e_possible_resolve s.dblist (List.hd s.localdb) secvars concl)
+                         (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl)
 	in
 	List.map
 	  (fun (lgls, cost, pp) ->
-- 
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/eauto.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/eauto.ml')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 6250fef2d6..0869ac0c76 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -478,7 +478,7 @@ let unfold_head env (ids, csts) c =
 	true, Environ.constant_value_in env c
     | App (f, args) ->
 	(match aux f with
-	| true, f' -> true, Reductionops.whd_betaiota Evd.empty (mkApp (f', args))
+	| true, f' -> true, Reductionops.whd_betaiota Evd.empty (EConstr.of_constr (mkApp (f', args)))
 	| false, _ -> 
 	    let done_, args' = 
 	      Array.fold_left_i (fun i (done_, acc) arg -> 
-- 
cgit v1.2.3


From cbea91d815f134d63d02d8fb1bd78ed97db28cd1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 19:52:48 +0100
Subject: Tacmach API using EConstr.

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

(limited to 'tactics/eauto.ml')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 0869ac0c76..2fad4fcf7f 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -30,7 +30,7 @@ let eauto_unif_flags = auto_flags_of_state full_transparent_state
 
 let e_give_exact ?(flags=eauto_unif_flags) c =
   Proofview.Goal.enter { enter = begin fun gl ->
-  let t1 = Tacmach.New.pf_unsafe_type_of gl c in
+  let t1 = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in
   let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
   let sigma = Tacmach.New.project gl in
   if occur_existential sigma (EConstr.of_constr t1) || occur_existential sigma (EConstr.of_constr t2) then
-- 
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/eauto.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tactics/eauto.ml')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 2fad4fcf7f..7b07c93097 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -31,9 +31,10 @@ let eauto_unif_flags = auto_flags_of_state full_transparent_state
 let e_give_exact ?(flags=eauto_unif_flags) c =
   Proofview.Goal.enter { enter = begin fun gl ->
   let t1 = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in
+  let t1 = EConstr.of_constr t1 in
   let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
   let sigma = Tacmach.New.project gl in
-  if occur_existential sigma (EConstr.of_constr t1) || occur_existential sigma (EConstr.of_constr t2) then
+  if occur_existential sigma t1 || occur_existential sigma (EConstr.of_constr t2) then
      Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
   else exact_check c
   end }
-- 
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/eauto.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'tactics/eauto.ml')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 7b07c93097..24e4de7506 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -29,8 +29,9 @@ open Proofview.Notations
 let eauto_unif_flags = auto_flags_of_state full_transparent_state
 
 let e_give_exact ?(flags=eauto_unif_flags) c =
+  let c = EConstr.of_constr c in
   Proofview.Goal.enter { enter = begin fun gl ->
-  let t1 = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in
+  let t1 = Tacmach.New.pf_unsafe_type_of gl c in
   let t1 = EConstr.of_constr t1 in
   let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
   let sigma = Tacmach.New.project gl in
@@ -77,7 +78,7 @@ let apply_tac_list tac glls =
 
 let one_step l gl =
   [Proofview.V82.of_tactic Tactics.intro]
-  @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl)))
+  @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map EConstr.mkVar (pf_ids_of_hyps gl)))
   @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l)
   @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl))
 
@@ -94,8 +95,9 @@ let prolog_tac l n =
   Proofview.V82.tactic begin fun gl ->
   let map c =
     let (c, sigma) = Tactics.run_delayed (pf_env gl) (project gl) c in
+    let c = EConstr.Unsafe.to_constr c in
     let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in
-    out_term c
+    EConstr.of_constr (out_term c)
   in
   let l = List.map map l in
   try (prolog l n gl)
@@ -114,6 +116,7 @@ let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
 let unify_e_resolve poly flags (c,clenv) =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
       let clenv', c = connect_hint_clenv poly c clenv gl in
+      let c = EConstr.of_constr c in
       Proofview.V82.tactic
 	(fun gls ->
 	 let clenv' = clenv_unique_resolver ~flags clenv' gls in
@@ -515,6 +518,7 @@ let autounfold_one db cl =
   let did, c' = unfold_head env st 
     (match cl with Some (id, _) -> Tacmach.New.pf_get_hyp_typ id gl | None -> concl) 
   in
+  let c' = EConstr.of_constr c' in
     if did then
       match cl with
       | Some hyp -> change_in_hyp None (make_change_arg c') hyp
-- 
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/eauto.ml | 32 +++++++++++++++-----------------
 1 file changed, 15 insertions(+), 17 deletions(-)

(limited to 'tactics/eauto.ml')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 24e4de7506..5d42ed2d55 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -29,7 +29,6 @@ open Proofview.Notations
 let eauto_unif_flags = auto_flags_of_state full_transparent_state
 
 let e_give_exact ?(flags=eauto_unif_flags) c =
-  let c = EConstr.of_constr c in
   Proofview.Goal.enter { enter = begin fun gl ->
   let t1 = Tacmach.New.pf_unsafe_type_of gl c in
   let t1 = EConstr.of_constr t1 in
@@ -40,7 +39,7 @@ let e_give_exact ?(flags=eauto_unif_flags) c =
   else exact_check c
   end }
 
-let assumption id = e_give_exact (mkVar id)
+let assumption id = e_give_exact (EConstr.mkVar id)
 
 let e_assumption =
   Proofview.Goal.enter { enter = begin fun gl ->
@@ -49,7 +48,7 @@ let e_assumption =
 
 let registered_e_assumption =
   Proofview.Goal.enter { enter = begin fun gl ->
-  Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id))
+  Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (EConstr.mkVar id))
               (Tacmach.New.pf_ids_of_hyps gl))
   end }
 
@@ -89,15 +88,14 @@ let rec prolog l n gl =
 
 let out_term = function
   | IsConstr (c, _) -> c
-  | IsGlobRef gr -> fst (Universes.fresh_global_instance (Global.env ()) gr)
+  | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance (Global.env ()) gr))
 
 let prolog_tac l n =
   Proofview.V82.tactic begin fun gl ->
   let map c =
     let (c, sigma) = Tactics.run_delayed (pf_env gl) (project gl) c in
-    let c = EConstr.Unsafe.to_constr c in
     let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in
-    EConstr.of_constr (out_term c)
+    out_term c
   in
   let l = List.map map l in
   try (prolog l n gl)
@@ -116,7 +114,6 @@ let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
 let unify_e_resolve poly flags (c,clenv) =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
       let clenv', c = connect_hint_clenv poly c clenv gl in
-      let c = EConstr.of_constr c in
       Proofview.V82.tactic
 	(fun gls ->
 	 let clenv' = clenv_unique_resolver ~flags clenv' gls in
@@ -124,13 +121,13 @@ let unify_e_resolve poly flags (c,clenv) =
 		 (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls)
     end }
 
-let hintmap_of secvars hdc concl =
+let hintmap_of sigma secvars hdc concl =
   match hdc with
   | None -> fun db -> Hint_db.map_none ~secvars db
   | Some hdc ->
-     if occur_existential Evd.empty (EConstr.of_constr concl) then (** FIXME *)
-       (fun db -> Hint_db.map_existential ~secvars hdc concl db)
-     else (fun db -> Hint_db.map_auto ~secvars hdc concl db)
+     if occur_existential sigma concl then
+       (fun db -> Hint_db.map_existential sigma ~secvars hdc concl db)
+     else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db)
    (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
 
 let e_exact poly flags (c,clenv) =
@@ -152,13 +149,13 @@ let rec e_trivial_fail_db db_list local_db =
   let tacl =
     registered_e_assumption ::
     (Tacticals.New.tclTHEN Tactics.intro next) ::
-    (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_nf_concl gl)))
+    (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (EConstr.of_constr (Tacmach.New.pf_nf_concl gl))))
   in
   Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
   end }
 
-and e_my_find_search db_list local_db secvars hdc concl =
-  let hint_of_db = hintmap_of secvars hdc concl in
+and e_my_find_search sigma db_list local_db secvars hdc concl =
+  let hint_of_db = hintmap_of sigma secvars hdc concl in
   let hintl =
       List.map_append (fun db ->
 	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
@@ -188,13 +185,13 @@ and e_my_find_search db_list local_db secvars hdc concl =
 
 and e_trivial_resolve sigma db_list local_db secvars gl =
   let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in
-  try priority (e_my_find_search db_list local_db secvars hd gl)
+  try priority (e_my_find_search sigma db_list local_db secvars hd gl)
   with Not_found -> []
 
 let e_possible_resolve sigma db_list local_db secvars gl =
   let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in
   try List.map (fun (b, (tac, pp)) -> (tac, b, pp))
-               (e_my_find_search db_list local_db secvars hd gl)
+               (e_my_find_search sigma db_list local_db secvars hd gl)
   with Not_found -> []
 
 let find_first_goal gls =
@@ -265,7 +262,7 @@ module SearchProblem = struct
       let g = find_first_goal lg in
       let hyps = pf_ids_of_hyps g in
       let secvars = secvars_of_hyps (pf_hyps g) in
-      let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in
+      let map_assum id = (e_give_exact (EConstr.mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in
       let assumption_tacs =
         let tacs = List.map map_assum hyps in
         let l = filter_tactics s.tacres tacs in
@@ -293,6 +290,7 @@ module SearchProblem = struct
       let rec_tacs =
 	let l =
           let concl = Reductionops.nf_evar (project g)(pf_concl g) in
+          let concl = EConstr.of_constr concl in
 	  filter_tactics s.tacres
                          (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl)
 	in
-- 
cgit v1.2.3


From e71f6d24465ea7812e9b893ed8e0deb2a44ce4f8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 00:28:38 +0100
Subject: Eauto API using EConstr.

---
 tactics/eauto.ml | 31 +++++++++++++++++--------------
 1 file changed, 17 insertions(+), 14 deletions(-)

(limited to 'tactics/eauto.ml')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 5d42ed2d55..986d1a624e 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -13,6 +13,7 @@ open Names
 open Nameops
 open Term
 open Termops
+open EConstr
 open Proof_type
 open Tacticals
 open Tacmach
@@ -33,13 +34,14 @@ let e_give_exact ?(flags=eauto_unif_flags) c =
   let t1 = Tacmach.New.pf_unsafe_type_of gl c in
   let t1 = EConstr.of_constr t1 in
   let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
+  let t2 = EConstr.of_constr t2 in
   let sigma = Tacmach.New.project gl in
-  if occur_existential sigma t1 || occur_existential sigma (EConstr.of_constr t2) then
+  if occur_existential sigma t1 || occur_existential sigma t2 then
      Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
   else exact_check c
   end }
 
-let assumption id = e_give_exact (EConstr.mkVar id)
+let assumption id = e_give_exact (mkVar id)
 
 let e_assumption =
   Proofview.Goal.enter { enter = begin fun gl ->
@@ -48,7 +50,7 @@ let e_assumption =
 
 let registered_e_assumption =
   Proofview.Goal.enter { enter = begin fun gl ->
-  Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (EConstr.mkVar id))
+  Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id))
               (Tacmach.New.pf_ids_of_hyps gl))
   end }
 
@@ -77,7 +79,7 @@ let apply_tac_list tac glls =
 
 let one_step l gl =
   [Proofview.V82.of_tactic Tactics.intro]
-  @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map EConstr.mkVar (pf_ids_of_hyps gl)))
+  @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl)))
   @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l)
   @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl))
 
@@ -262,7 +264,7 @@ module SearchProblem = struct
       let g = find_first_goal lg in
       let hyps = pf_ids_of_hyps g in
       let secvars = secvars_of_hyps (pf_hyps g) in
-      let map_assum id = (e_give_exact (EConstr.mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in
+      let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in
       let assumption_tacs =
         let tacs = List.map map_assum hyps in
         let l = filter_tactics s.tacres tacs in
@@ -469,18 +471,18 @@ let autounfold_tac db cls =
   in
   autounfold dbs cls
 
-let unfold_head env (ids, csts) c = 
+let unfold_head env sigma (ids, csts) c =
   let rec aux c = 
-    match kind_of_term c with
+    match EConstr.kind sigma c with
     | Var id when Id.Set.mem id ids ->
 	(match Environ.named_body id env with
-	| Some b -> true, b
+	| Some b -> true, EConstr.of_constr b
 	| None -> false, c)
     | Const (cst,u as c) when Cset.mem cst csts ->
-	true, Environ.constant_value_in env c
+	true, EConstr.of_constr (Environ.constant_value_in env c)
     | App (f, args) ->
 	(match aux f with
-	| true, f' -> true, Reductionops.whd_betaiota Evd.empty (EConstr.of_constr (mkApp (f', args)))
+	| true, f' -> true, EConstr.of_constr (Reductionops.whd_betaiota sigma (mkApp (f', args)))
 	| false, _ -> 
 	    let done_, args' = 
 	      Array.fold_left_i (fun i (done_, acc) arg -> 
@@ -494,7 +496,7 @@ let unfold_head env (ids, csts) c =
 	      else false, c)
     | _ -> 
 	let done_ = ref false in
-	let c' = map_constr (fun c -> 
+	let c' = EConstr.map sigma (fun c -> 
 	  if !done_ then c else 
 	    let x, c' = aux c in
 	      done_ := x; c') c
@@ -504,7 +506,9 @@ let unfold_head env (ids, csts) c =
 let autounfold_one db cl =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
+  let sigma = Tacmach.New.project gl in
   let concl = Proofview.Goal.concl gl in
+  let concl = EConstr.of_constr concl in
   let st =
     List.fold_left (fun (i,c) dbname -> 
       let db = try searchtable_map dbname 
@@ -513,10 +517,9 @@ let autounfold_one db cl =
       let (ids, csts) = Hint_db.unfolds db in
 	(Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db
   in
-  let did, c' = unfold_head env st 
-    (match cl with Some (id, _) -> Tacmach.New.pf_get_hyp_typ id gl | None -> concl) 
+  let did, c' = unfold_head env sigma st 
+    (match cl with Some (id, _) -> EConstr.of_constr (Tacmach.New.pf_get_hyp_typ id gl) | None -> concl) 
   in
-  let c' = EConstr.of_constr c' in
     if did then
       match cl with
       | Some hyp -> change_in_hyp None (make_change_arg c') hyp
-- 
cgit v1.2.3


From e09f3b44bb381854b647a6d9debdeddbfc49177e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 22:16:08 +0100
Subject: Proofview.Goal primitive now return EConstrs.

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

(limited to 'tactics/eauto.ml')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 986d1a624e..57400d3340 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -34,7 +34,6 @@ let e_give_exact ?(flags=eauto_unif_flags) c =
   let t1 = Tacmach.New.pf_unsafe_type_of gl c in
   let t1 = EConstr.of_constr t1 in
   let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
-  let t2 = EConstr.of_constr t2 in
   let sigma = Tacmach.New.project gl in
   if occur_existential sigma t1 || occur_existential sigma t2 then
      Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
@@ -151,7 +150,7 @@ let rec e_trivial_fail_db db_list local_db =
   let tacl =
     registered_e_assumption ::
     (Tacticals.New.tclTHEN Tactics.intro next) ::
-    (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (EConstr.of_constr (Tacmach.New.pf_nf_concl gl))))
+    (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_nf_concl gl)))
   in
   Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
   end }
@@ -508,7 +507,6 @@ let autounfold_one db cl =
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let concl = Proofview.Goal.concl gl in
-  let concl = EConstr.of_constr concl in
   let st =
     List.fold_left (fun (i,c) dbname -> 
       let db = try searchtable_map dbname 
-- 
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/eauto.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/eauto.ml')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 57400d3340..92e59c5ce4 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -481,7 +481,7 @@ let unfold_head env sigma (ids, csts) c =
 	true, EConstr.of_constr (Environ.constant_value_in env c)
     | App (f, args) ->
 	(match aux f with
-	| true, f' -> true, EConstr.of_constr (Reductionops.whd_betaiota sigma (mkApp (f', args)))
+	| true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args))
 	| false, _ -> 
 	    let done_, args' = 
 	      Array.fold_left_i (fun i (done_, acc) arg -> 
-- 
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/eauto.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'tactics/eauto.ml')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 92e59c5ce4..01f21910cf 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -32,7 +32,6 @@ let eauto_unif_flags = auto_flags_of_state full_transparent_state
 let e_give_exact ?(flags=eauto_unif_flags) c =
   Proofview.Goal.enter { enter = begin fun gl ->
   let t1 = Tacmach.New.pf_unsafe_type_of gl c in
-  let t1 = EConstr.of_constr t1 in
   let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
   let sigma = Tacmach.New.project gl in
   if occur_existential sigma t1 || occur_existential sigma t2 then
@@ -290,7 +289,7 @@ module SearchProblem = struct
       in
       let rec_tacs =
 	let l =
-          let concl = Reductionops.nf_evar (project g)(pf_concl g) in
+          let concl = Reductionops.nf_evar (project g) (EConstr.Unsafe.to_constr (pf_concl g)) in
           let concl = EConstr.of_constr concl in
 	  filter_tactics s.tacres
                          (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl)
@@ -516,7 +515,7 @@ let autounfold_one db cl =
 	(Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db
   in
   let did, c' = unfold_head env sigma st 
-    (match cl with Some (id, _) -> EConstr.of_constr (Tacmach.New.pf_get_hyp_typ id gl) | None -> concl) 
+    (match cl with Some (id, _) -> Tacmach.New.pf_get_hyp_typ id gl | None -> concl) 
   in
     if did then
       match cl with
-- 
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/eauto.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'tactics/eauto.ml')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 01f21910cf..7453fff5c3 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -289,8 +289,7 @@ module SearchProblem = struct
       in
       let rec_tacs =
 	let l =
-          let concl = Reductionops.nf_evar (project g) (EConstr.Unsafe.to_constr (pf_concl g)) in
-          let concl = EConstr.of_constr concl in
+          let concl = Reductionops.nf_evar (project g) (pf_concl g) in
 	  filter_tactics s.tacres
                          (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl)
 	in
-- 
cgit v1.2.3


From 3c1cd2338fcddc4a6c0e97b0af53eb2b2f238c4a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 15 Dec 2016 10:45:19 +0100
Subject: Removing most nf_enter in tactics.

Now they are useless because all of the primitives are (should?) be
evar-insensitive.
---
 tactics/eauto.ml | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

(limited to 'tactics/eauto.ml')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 7453fff5c3..14082bb8dc 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -112,13 +112,12 @@ open Auto
 let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
 
 let unify_e_resolve poly flags (c,clenv) =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
       let clenv', c = connect_hint_clenv poly c clenv gl in
-      Proofview.V82.tactic
-	(fun gls ->
-	 let clenv' = clenv_unique_resolver ~flags clenv' gls in
-	 tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
-		 (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls)
+      let clenv' = clenv_unique_resolver ~flags clenv' gl in
+      Proofview.tclTHEN
+        (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
+        (Tactics.Simple.eapply c)
     end }
 
 let hintmap_of sigma secvars hdc concl =
@@ -139,7 +138,7 @@ let e_exact poly flags (c,clenv) =
   end }
 
 let rec e_trivial_fail_db db_list local_db =
-  let next = Proofview.Goal.nf_enter { enter = begin fun gl ->
+  let next = Proofview.Goal.enter { enter = begin fun gl ->
     let d = Tacmach.New.pf_last_hyp gl in
     let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Tacmach.New.project gl) d in
     e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Tacmach.New.project gl) hintl local_db)
@@ -149,7 +148,7 @@ let rec e_trivial_fail_db db_list local_db =
   let tacl =
     registered_e_assumption ::
     (Tacticals.New.tclTHEN Tactics.intro next) ::
-    (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_nf_concl gl)))
+    (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl)))
   in
   Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
   end }
@@ -501,7 +500,7 @@ let unfold_head env sigma (ids, csts) c =
   in aux c
 
 let autounfold_one db cl =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let concl = Proofview.Goal.concl gl in
-- 
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.
---
 tactics/eauto.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'tactics/eauto.ml')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index e0dff3739d..8d1e0e507a 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -472,8 +472,9 @@ let unfold_head env sigma (ids, csts) c =
 	(match Environ.named_body id env with
 	| Some b -> true, EConstr.of_constr b
 	| None -> false, c)
-    | Const (cst,u as c) when Cset.mem cst csts ->
-	true, EConstr.of_constr (Environ.constant_value_in env c)
+    | Const (cst, u) when Cset.mem cst csts ->
+        let u = EInstance.kind sigma u in
+	true, EConstr.of_constr (Environ.constant_value_in env (cst, u))
     | App (f, args) ->
 	(match aux f with
 	| true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args))
-- 
cgit v1.2.3