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.

---
 plugins/cc/ccalgo.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/cc/ccalgo.ml')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index bc53b113df..102efe55bc 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -508,7 +508,7 @@ let rec add_term state t=
 	Not_found ->
 	  let b=next uf in
           let trm = constr_of_term t in
-	  let typ = pf_unsafe_type_of state.gls trm in
+	  let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in
 	  let typ = canonize_name typ in
 	  let new_node=
 	    match t with
@@ -832,7 +832,7 @@ let complete_one_class state i=
 	    let id = new_state_var etyp state in
 		app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
 	let _c = pf_unsafe_type_of state.gls
-	  (constr_of_term (term state.uf pac.cnode)) in
+	  (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
 	let _args =
 	  List.map (fun i -> constr_of_term (term state.uf  i))
 	    pac.args in
-- 
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.

---
 plugins/cc/ccalgo.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/cc/ccalgo.ml')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 102efe55bc..0a980c03b7 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -497,10 +497,10 @@ let rec inst_pattern subst = function
 	   args t
 
 let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++
-  Termops.print_constr (constr_of_term (term uf i)) ++ str "]"
+  Termops.print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
 
 let pr_term t = str "[" ++
-  Termops.print_constr (constr_of_term t) ++ str "]"
+  Termops.print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]"
 
 let rec add_term state t=
   let uf=state.uf in
@@ -615,7 +615,7 @@ let add_inst state (inst,int_subst) =
 	      begin
 		debug (fun () ->
 		   (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
-	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
+	          (str "  [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++
 			   pr_term s ++ str " == " ++ pr_term t ++ str "]"));
 		add_equality state prf s t
 	      end
@@ -623,7 +623,7 @@ let add_inst state (inst,int_subst) =
 	      begin
 		debug (fun () ->
 		   (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
-	          (str "  [" ++ Termops.print_constr prf ++ str " : " ++
+	          (str "  [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++
 			   pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
 		add_disequality state (Hyp prf) s t
 	      end
-- 
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.

---
 plugins/cc/ccalgo.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'plugins/cc/ccalgo.ml')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 0a980c03b7..aedcb75750 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -452,8 +452,9 @@ and applist_projection c l =
       applistc (mkProj (p, hd)) tl)
   | _ -> applistc c l
 
-let rec canonize_name c =
-  let func =  canonize_name in
+let rec canonize_name sigma c =
+  let c = EConstr.Unsafe.to_constr c in
+  let func c = canonize_name sigma (EConstr.of_constr c) in
     match kind_of_term c with
       | Const (kn,u) ->
 	  let canon_const = constant_of_kn (canonical_con kn) in 
@@ -509,7 +510,7 @@ let rec add_term state t=
 	  let b=next uf in
           let trm = constr_of_term t in
 	  let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in
-	  let typ = canonize_name typ in
+	  let typ = canonize_name (project state.gls) typ in
 	  let new_node=
 	    match t with
 		Symb _ | Product (_,_) ->
@@ -833,6 +834,7 @@ let complete_one_class state i=
 		app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
 	let _c = pf_unsafe_type_of state.gls
 	  (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
+        let _c = EConstr.Unsafe.to_constr _c in
 	let _args =
 	  List.map (fun i -> constr_of_term (term state.uf  i))
 	    pac.args in
-- 
cgit v1.2.3