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).
---
 plugins/ltac/extratactics.ml4 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index d68139a4b4..cba9c13648 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -636,7 +636,7 @@ let subst_var_with_hole occ tid t =
            else
 	     (incr locref;
               CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
-	      GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),
+	      GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),
                      Misctypes.IntroAnonymous, None)))
         else x
     | c -> map_glob_constr_left_to_right substrec c in
@@ -648,13 +648,13 @@ let subst_hole_with_term occ tc t =
   let locref = ref 0 in
   let occref = ref occ in
   let rec substrec = function
-    | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) } ->
+    | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) } ->
         decr occref;
         if Int.equal !occref 0 then tc
         else
 	  (incr locref;
            CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
-	   GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s))
+	   GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s))
     | c -> map_glob_constr_left_to_right substrec c
   in
   substrec t
-- 
cgit v1.2.3