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