From bbde815f8108f4641f5411d03f7a88096cc2221b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 24 May 2017 21:55:21 +0200
Subject: Support for using type information to infer more precise evar
 sources.

This allows a better control on the name to give to an evar and, in
particular, to address the issue about naming produced by "epose
proof" in one of the comment of Zimmi48 at PR #248 (see file names.v).

Incidentally updating output of Show output test (evar numbers shifted).
---
 pretyping/cases.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'pretyping/cases.ml')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c2c8065a98..4261573725 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2064,8 +2064,8 @@ let mk_JMeq evdref typ x typ' y =
 let mk_JMeq_refl evdref typ x = 
   papp evdref coq_JMeq_refl [| typ; x |]
 
-let hole = CAst.make @@
-  GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false),
+let hole na = CAst.make @@
+  GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na),
          Misctypes.IntroAnonymous, None)
 
 let constr_of_pat env evdref arsign pat avoid =
@@ -2168,7 +2168,7 @@ let vars_of_ctx sigma ctx =
 	    prev,
 	    (CAst.make @@ GApp (
 		(CAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), 
-		   [hole; CAst.make @@ GVar prev])) :: vars
+		   [hole na; CAst.make @@ GVar prev])) :: vars
 	| _ ->
 	    match RelDecl.get_name decl with
 		Anonymous -> invalid_arg "vars_of_ctx"
@@ -2301,7 +2301,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	       | l  -> CAst.make @@ GApp (bref, l)
 	 in
 	 let branch = match ineqs with
-	     Some _ -> CAst.make @@ GApp (branch, [ hole ])
+	     Some _ -> CAst.make @@ GApp (branch, [ hole Anonymous ])
 	   | None -> branch
 	 in
 	 incr i;
-- 
cgit v1.2.3