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/term_dnet.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/term_dnet.ml')

diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index e4b45489dc..6294f9fdc2 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -351,7 +351,7 @@ struct
       (fun id acc ->
 	 let c_id = Opt.reduce (Ident.constr_of id) in
 	 let (ctx,wc) =
-	   try Termops.align_prod_letin whole_c c_id
+	   try Termops.align_prod_letin Evd.empty (EConstr.of_constr whole_c) (EConstr.of_constr c_id) (** FIXME *)
 	   with Invalid_argument _ -> [],c_id in
 	 let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in
 	 try
-- 
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/term_dnet.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/term_dnet.ml')

diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 6294f9fdc2..38342b64dc 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -355,7 +355,7 @@ struct
 	   with Invalid_argument _ -> [],c_id in
 	 let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in
 	 try
-          let _ = Termops.filtering ctx Reduction.CUMUL wc whole_c in
+          let _ = Termops.filtering Evd.empty ctx Reduction.CUMUL wc whole_c in
           id :: acc
 	 with Termops.CannotFilter -> (* msgnl(str"recon "++Termops.print_constr_env (Global.env()) wc); *) acc
       ) (TDnet.find_match dpat dn) []
-- 
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/term_dnet.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'tactics/term_dnet.ml')

diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 38342b64dc..219abb7fdd 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -350,9 +350,11 @@ struct
     TDnet.Idset.fold
       (fun id acc ->
 	 let c_id = Opt.reduce (Ident.constr_of id) in
+	 let c_id = EConstr.of_constr c_id in
 	 let (ctx,wc) =
-	   try Termops.align_prod_letin Evd.empty (EConstr.of_constr whole_c) (EConstr.of_constr c_id) (** FIXME *)
+	   try Termops.align_prod_letin Evd.empty (EConstr.of_constr whole_c) c_id (** FIXME *)
 	   with Invalid_argument _ -> [],c_id in
+          let wc = EConstr.Unsafe.to_constr wc in
 	 let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in
 	 try
           let _ = Termops.filtering Evd.empty ctx Reduction.CUMUL wc whole_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/term_dnet.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'tactics/term_dnet.ml')

diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 219abb7fdd..2c863c42a6 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -344,7 +344,7 @@ struct
     ) (pr_dconstr pr_term_pattern) p*)
 
   let search_pat cpat dpat dn =
-    let whole_c = cpat in
+    let whole_c = EConstr.of_constr cpat in
     (* if we are at the root, add an empty context *)
     let dpat = under_prod (empty_ctx dpat) in
     TDnet.Idset.fold
@@ -352,9 +352,8 @@ struct
 	 let c_id = Opt.reduce (Ident.constr_of id) in
 	 let c_id = EConstr.of_constr c_id in
 	 let (ctx,wc) =
-	   try Termops.align_prod_letin Evd.empty (EConstr.of_constr whole_c) c_id (** FIXME *)
+	   try Termops.align_prod_letin Evd.empty whole_c c_id (** FIXME *)
 	   with Invalid_argument _ -> [],c_id in
-          let wc = EConstr.Unsafe.to_constr wc in
 	 let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in
 	 try
           let _ = Termops.filtering Evd.empty ctx Reduction.CUMUL wc whole_c in
-- 
cgit v1.2.3