From e4f066238799a4598817dfeab8a044760ab670de Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 7 Nov 2016 20:33:06 +0100
Subject: Coercion API using EConstr.

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

(limited to 'pretyping/program.ml')

diff --git a/pretyping/program.ml b/pretyping/program.ml
index 4b6137b539..2606d91f35 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -29,8 +29,9 @@ let init_constant dir s () = coq_constant "Program" dir s
 let init_reference dir s () = coq_reference "Program" dir s
 
 let papp evdref r args = 
+  let open EConstr in
   let gr = delayed_force r in
-    mkApp (Evarutil.e_new_global evdref gr, args)
+    mkApp (EConstr.of_constr (Evarutil.e_new_global evdref gr), args)
 
 let sig_typ = init_reference ["Init"; "Specif"] "sig"
 let sig_intro = init_reference ["Init"; "Specif"] "exist"
-- 
cgit v1.2.3


From 67dc22d8389234d0c9b329944ff579e7056b7250 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 8 Nov 2016 10:57:05 +0100
Subject: Cases API using EConstr.

---
 pretyping/program.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'pretyping/program.ml')

diff --git a/pretyping/program.ml b/pretyping/program.ml
index 2606d91f35..8ec6083f71 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -58,7 +58,9 @@ let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl"
 let coq_not = init_constant ["Init";"Logic"] "not"
 let coq_and = init_constant ["Init";"Logic"] "and"
 
-let mk_coq_not x = mkApp (delayed_force coq_not, [| x |])
+let delayed_force c = EConstr.of_constr (c ())
+
+let mk_coq_not x = EConstr.mkApp (delayed_force coq_not, [| x |])
 
 let unsafe_fold_right f = function
     hd :: tl -> List.fold_right f tl hd
@@ -68,7 +70,7 @@ let mk_coq_and l =
   let and_typ = delayed_force coq_and in
     unsafe_fold_right
       (fun c conj ->
-	 mkApp (and_typ, [| c ; conj |]))
+	 EConstr.mkApp (and_typ, [| c ; conj |]))
       l
 
 (* true = transparent by default, false = opaque if possible *)
-- 
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.

---
 pretyping/program.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/program.ml')

diff --git a/pretyping/program.ml b/pretyping/program.ml
index 8ec6083f71..caa5a5c8a6 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -31,7 +31,7 @@ let init_reference dir s () = coq_reference "Program" dir s
 let papp evdref r args = 
   let open EConstr in
   let gr = delayed_force r in
-    mkApp (EConstr.of_constr (Evarutil.e_new_global evdref gr), args)
+    mkApp (Evarutil.e_new_global evdref gr, args)
 
 let sig_typ = init_reference ["Init"; "Specif"] "sig"
 let sig_intro = init_reference ["Init"; "Specif"] "exist"
-- 
cgit v1.2.3