Referring to evars by names. Added a parser for evars (but parsing of

instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.

4 files changed, 39 insertions, 7 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index c6f0f2ee0..6f607133d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -270,6 +270,33 @@ let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
     clenv_unify CUMUL ~flags
       (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv
 
+let adjust_meta_source evd mv = function
+  | loc,Evar_kinds.VarInstance id ->
+    let rec match_name c l =
+      match kind_of_term c, l with
+      | Lambda (Name id,_,c), a::l when Constr.equal a (mkMeta mv) -> Some id
+      | Lambda (_,_,c), a::l -> match_name c l
+      | _ -> None in
+    (* This is very ad hoc code so that an evar inherits the name of the binder
+       in situations like "ex_intro (fun x => P) ?ev p" *)
+    let f = function (mv',(Cltyp (_,t) | Clval (_,_,t))) ->
+      if Metaset.mem mv t.freemetas then
+        let f,l = decompose_app t.rebus in
+        match kind_of_term f with
+        | Meta mv'' ->
+          (match meta_opt_fvalue evd mv'' with
+          | Some (c,_) -> match_name c.rebus l
+          | None -> None)
+        | Evar ev ->
+          (match existential_opt_value evd ev with
+          | Some c -> match_name c l
+          | None -> None)
+        | _ -> None
+      else None in
+    let id = try List.find_map f (Evd.meta_list evd) with Not_found -> id in
+    loc,Evar_kinds.VarInstance id
+  | src -> src
+
 (* [clenv_pose_metas_as_evars clenv dep_mvs]
  * For each dependent evar in the clause-env which does not have a value,
  * pose a value for it by constructing a fresh evar.  We do this in
@@ -306,8 +333,10 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
       (* This assumes no cycle in the dependencies - is it correct ? *)
       if occur_meta ty then fold clenv (mvs@[mv])
       else
+        let src = evar_source_of_meta mv clenv.evd in
+        let src = adjust_meta_source clenv.evd mv src in
 	let (evd,evar) =
-	  new_evar clenv.evd (cl_env clenv) ~src:(Loc.ghost,Evar_kinds.GoalEvar) ty in
+	  new_evar clenv.evd (cl_env clenv) ~src ty in
 	let clenv = clenv_assign mv evar {clenv with evd=evd} in
 	fold clenv mvs in
   fold clenv dep_mvs
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 98a97a91c..5f97e72fa 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -23,7 +23,9 @@ let depends_on_evar evk _ (pbty,_,t1,t2) =
   try Evar.equal (head_evar t2) evk
   with NoHeadEvar -> false
 
-let define_and_solve_constraints evk c evd =
+let define_and_solve_constraints evk c env evd =
+  if Termops.occur_evar evk c then
+    Pretype_errors.error_occur_check env evd evk c;
   let evd = define evk c evd in
   let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in
   match
@@ -55,7 +57,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
         (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
 			string_of_existential evk))
   in
-  define_and_solve_constraints evk typed_c (evars_reset_evd sigma' sigma)
+  define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma)
 
 (* vernac command Existential *)
 
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 19a1f7758..4df280e23 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -254,12 +254,12 @@ let db_mc_pattern_success debug =
   else return ()
 
 (* Prints a failure message for an hypothesis pattern *)
-let db_hyp_pattern_failure debug env (na,hyp) =
+let db_hyp_pattern_failure debug env sigma (na,hyp) =
   is_debug debug >>= fun db ->
   if db then
     msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^
                 " cannot match: ") ++
-           Hook.get prmatchpatt env hyp)
+           Hook.get prmatchpatt env sigma hyp)
   else return ()
 
 (* Prints a matching failure message for a rule *)
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index bf8507360..864739089 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -11,6 +11,7 @@ open Pattern
 open Names
 open Tacexpr
 open Term
+open Evd
 
 (** This module intends to be a beginning of debugger for tactic expressions.
    Currently, it is quite simple and we can hope to have, in the future, a more
@@ -18,7 +19,7 @@ open Term
 
 val tactic_printer : (glob_tactic_expr -> Pp.std_ppcmds) Hook.t
 val match_pattern_printer :
-  (env -> constr_pattern match_pattern -> Pp.std_ppcmds) Hook.t
+  (env -> evar_map -> constr_pattern match_pattern -> Pp.std_ppcmds) Hook.t
 val match_rule_printer :
   ((Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) Hook.t
 
@@ -53,7 +54,7 @@ val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t
 
 (** Prints a failure message for an hypothesis pattern *)
 val db_hyp_pattern_failure :
-  debug_info -> env -> Name.t * constr_pattern match_pattern -> unit Proofview.NonLogical.t
+  debug_info -> env -> evar_map -> Name.t * constr_pattern match_pattern -> unit Proofview.NonLogical.t
 
 (** Prints a matching failure message for a rule *)
 val db_matching_failure : debug_info -> unit Proofview.NonLogical.t