From 1c10b84c0ce5f96a3afd1fc83c738c76070958c3 Mon Sep 17 00:00:00 2001
From: amblaf
Date: Tue, 27 Jun 2017 08:38:20 +0200
Subject: Correcting [build_discriminator] to make the test-suite pass

---
 API/API.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index 19726b52f2..3905843a55 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5233,7 +5233,7 @@ sig
 
   val build_selector :
     Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.types ->
-    EConstr.constr -> EConstr.constr -> Evd.evar_map * EConstr.constr
+    EConstr.constr -> EConstr.constr -> EConstr.constr
   val replace : EConstr.constr -> EConstr.constr -> unit Proofview.tactic
   val general_rewrite :
     orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag ->
-- 
cgit v1.2.3