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