From 9d47cc0af706ed1cd4ab87c2d402a0457a9b6a5c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 19 Nov 2015 17:48:32 +0100
Subject: Fix bug #4433, removing hack on evars appearing in a pattern from a
 constr, and the associated signature, not needed anymore. Update CHANGES, no
 evar_map is produced by pattern_of_constr anymore.

---
 pretyping/patternops.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'pretyping/patternops.mli')

diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 9e72280fe2..0148280287 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -39,8 +39,7 @@ val head_of_constr_reference : Term.constr -> global_reference
    a pattern; currently, no destructor (Cases, Fix, Cofix) and no
    existential variable are allowed in [c] *)
 
-val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> 
-  Evd.evar_map * named_context * constr_pattern
+val pattern_of_constr : Environ.env -> Evd.evar_map -> constr -> constr_pattern
 
 (** [pattern_of_glob_constr l c] translates a term [c] with metavariables into
    a pattern; variables bound in [l] are replaced by the pattern to which they
-- 
cgit v1.2.3