From d6bcc6ebe4f65d0555414851f7e4fb6fa1fb22a4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 22 Jan 2017 15:05:08 +0100
Subject: Adding a new evar source to remember the name of evars which were
 named in the original term.

Useful at least for debugging, useful to give a better message than
"this placeholder", even if in the loc is known in this case.
---
 interp/constrintern.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 235e6e24f6..c102d8e117 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1739,7 +1739,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         let k = match k with
         | None ->
            let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
-           Evar_kinds.QuestionMark st
+           (match naming with
+           | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id
+           | _ -> Evar_kinds.QuestionMark st)
         | Some k -> k
         in
         let solve = match solve with
-- 
cgit v1.2.3


From 180775636f5ec93e95df681951fafb321f8ebe67 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 26 Jan 2017 00:53:23 +0100
Subject: Fixing #5326 (anomaly on some unsupported case of 'pat).

We complete the support of 'pat in this particular case (a 'pat under
a binder in a notation).
---
 interp/topconstr.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 79eeacf354..d388376bc2 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -92,8 +92,9 @@ let rec fold_local_binders g f n acc b = function
       f n (fold_local_binders g f n' acc b l) t
   | LocalRawDef ((_,na),t)::l ->
       f n (fold_local_binders g f (name_fold g na n) acc b l) t
-  | LocalPattern _::l ->
-      assert false
+  | LocalPattern (_,pat,t)::l ->
+      let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
+      Option.fold_left (f n) acc t
   | [] ->
       f n acc b
 
-- 
cgit v1.2.3