Moving implicit tactic support from Tacinterp to Pfedit and final evar

resolution from Tacinterp to Pretyping (close to resolve_evars) so
that final evar resolution can eventually be called from Tactics.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14496 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 29 insertions, 3 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ad15ff903..2c85a26fe 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -165,7 +165,26 @@ let build_constant_by_tactic id sign typ tac =
     delete_current_proof ();
     raise e
 
-let build_by_tactic typ tac =
+let build_by_tactic env typ tac =
   let id = id_of_string ("temporary_proof"^string_of_int (next())) in
-  let sign = Decls.clear_proofs (Global.named_context ()) in
+  let sign = Decls.clear_proofs (named_context env) in
   (build_constant_by_tactic id sign typ tac).const_entry_body
+
+(**********************************************************************)
+(* Support for resolution of evars in tactic interpretation, including
+   resolution by application of tactics *)
+
+let implicit_tactic = ref None
+
+let declare_implicit_tactic tac = implicit_tactic := Some tac
+
+let solve_by_implicit_tactic env sigma (evk,args) =
+  let evi = Evd.find_undefined sigma evk in
+  match (!implicit_tactic, snd (evar_source evk sigma)) with
+  | Some tac, (ImplicitArg _ | QuestionMark _)
+      when
+	Sign.named_context_equal (Environ.named_context_of_val evi.evar_hyps)
+	(Environ.named_context env) ->
+      (try build_by_tactic env evi.evar_concl (tclCOMPLETE tac)
+       with e when Logic.catchable_exception e -> raise Exit)
+  | _ -> raise Exit
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 2453cb39b..289e8c13c 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -177,4 +177,11 @@ val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit
 
 val build_constant_by_tactic : identifier -> named_context_val -> types -> tactic ->
   Entries.definition_entry
-val build_by_tactic : types -> tactic -> constr
+val build_by_tactic : env -> types -> tactic -> constr
+
+(** Declare the default tactic to fill implicit arguments *)
+
+val declare_implicit_tactic : tactic -> unit
+
+(* Raise Exit if cannot solve *)
+val solve_by_implicit_tactic : env -> Evd.evar_map -> existential -> constr