From 77e638121b6683047be915da9d0499a58fcb6e52 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Nov 2016 19:30:24 +0100
Subject: Patternops API using EConstr.

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

(limited to 'pretyping/patternops.mli')

diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 1f63565d6f..93d2c859a9 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Term
+open EConstr
 open Globnames
 open Glob_term
 open Mod_subst
@@ -32,7 +33,7 @@ val head_pattern_bound : constr_pattern -> global_reference
 (** [head_of_constr_reference c] assumes [r] denotes a reference and
    returns its label; raises an anomaly otherwise *)
 
-val head_of_constr_reference : Term.constr -> global_reference
+val head_of_constr_reference : Evd.evar_map -> constr -> global_reference
 
 (** [pattern_of_constr c] translates a term [c] with metavariables into
    a pattern; currently, no destructor (Cases, Fix, Cofix) and no
-- 
cgit v1.2.3


From 5db9588098f9f02d923c21f3914e3c671b10728f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 24 Jan 2017 13:07:11 +0100
Subject: Quick hack to fix interpretation of patterns in Ltac.

Interpretation of patterns in Ltac is essentially flawed. It does a roundtrip
through the pretyper, and relies on suspicious flagging of evars in the evar source
field to recognize original pattern holes. After the pattern_of_constr function
was made evar-insensitive, it expanded evars that were solved by magical side-effects
of the pretyper, even if it hadn't been asked to perform any heuristics.

We backtrack on the insensitivity of the pattern_of_constr function. This may have
a performance penalty in other dubious code, e.g. hints. In the long run we should
get rid of the pattern_of_constr function.
---
 pretyping/patternops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/patternops.mli')

diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 93d2c859a9..5694d345c1 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -39,7 +39,7 @@ val head_of_constr_reference : Evd.evar_map -> 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 -> constr_pattern
+val pattern_of_constr : Environ.env -> Evd.evar_map -> Constr.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