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).
---
 vernac/command.ml     | 2 +-
 vernac/obligations.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index e2ebb4d7fb..25dd724af8 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -1062,7 +1062,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
     mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force fix_sub_ref)),
 	  [| argtyp ; wf_rel ;
 	     Evarutil.e_new_evar env evdref
-	       ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
+	       ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof;
 	     prop |])
   in
   let def = Typing.e_solve_evars env evdref def in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index be58c67a9e..47ac16f9c7 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -221,7 +221,7 @@ let eterm_obligations env name evm fs ?status t ty =
 	 in
 	 let loc, k = evar_source id evm in
 	 let status = match k with
-           | Evar_kinds.QuestionMark o -> o
+           | Evar_kinds.QuestionMark (o,_) -> o
            | _ -> match status with
                  | Some o -> o
                  | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ()))
-- 
cgit v1.2.3