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/pretyping.ml | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'pretyping/pretyping.ml')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e72394fa28..b0663af70c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -383,6 +383,21 @@ let process_inference_flags flags env initial_sigma (sigma,c) =
   let c = if flags.expand_evars then nf_evar sigma c else c in
   sigma,c
 
+let adjust_evar_source evdref na c =
+  match na, kind !evdref c with
+  | Name id, Evar (evk,args) ->
+     let evi = Evd.find !evdref evk in
+     begin match evi.evar_source with
+     | loc, Evar_kinds.QuestionMark (b,Anonymous) ->
+        let src = (loc,Evar_kinds.QuestionMark (b,na)) in
+        let sigma = Sigma.Unsafe.of_evar_map !evdref in
+        let Sigma (evk', evd, _) = restrict_evar sigma evk (evar_filter evi) ~src None in
+        evdref := Sigma.to_evar_map evd;
+        mkEvar (evk',args)
+     | _ -> c
+     end
+  | _, _ -> c
+
 (* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
 let allow_anonymous_refs = ref false
 
@@ -785,6 +800,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 		  args, nf_evar !evdref (j_val hj)
 		else [], j_val hj
 	    in
+            let ujval = adjust_evar_source evdref na ujval in
 	    let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in
 	    let j = { uj_val = value; uj_type = typ } in
 	      apply_rec env (n+1) j candargs rest
-- 
cgit v1.2.3