From 563d173d86cb8fbaccad70ee4c665aa60beb069c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 29 May 2017 18:54:46 +0200
Subject: Pretyping cleanup: remove constr_of_global calls

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

(limited to 'pretyping/program.mli')

diff --git a/pretyping/program.mli b/pretyping/program.mli
index 94a7bdcb6d..8439b9528c 100644
--- a/pretyping/program.mli
+++ b/pretyping/program.mli
@@ -32,8 +32,8 @@ val coq_eq_rect : unit -> global_reference
 val coq_JMeq_ind : unit -> global_reference
 val coq_JMeq_refl : unit -> global_reference
 
-val mk_coq_and : constr list -> constr
-val mk_coq_not : constr -> constr
+val mk_coq_and : Evd.evar_map -> constr list -> Evd.evar_map * constr
+val mk_coq_not : Evd.evar_map -> constr -> Evd.evar_map * constr
 
 (** Polymorphic application of delayed references *)
 val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr
-- 
cgit v1.2.3