Optional callbacks have been added to tactics that need to introduce

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 396c968fd99e170eb100854f0bd3c0f341bc41bd..a94472bf2f87f45a7b61ee76197d6cfcc6e4c598 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1658,6 +1658,22 @@ let new_inductive () =
       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
+let mk_fresh_name_callback context name ~typ =
+ let fresh_name =
+  match ProofEngineHelpers.mk_fresh_name context name ~typ with
+     Cic.Name fresh_name -> fresh_name
+   | Cic.Anonymous -> assert false
+ in
+  match
+   GToolbox.input_string ~title:"Enter a fresh hypothesis name" ~text:fresh_name
+    ("Enter a fresh name for the hypothesis " ^
+      CicPp.pp typ
+       (List.map (function None -> None | Some (n,_) -> Some n) context))
+  with
+     Some fresh_name' -> Cic.Name fresh_name'
+   | None -> raise NoChoice
+;;
+
 let new_proof () =
  let inputt = ((rendering_window ())#inputt : term_editor) in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
@@ -1758,7 +1774,10 @@ let new_proof () =
      refresh_sequent notebook ;
      refresh_proof output ;
      !save_set_sensitive true ;
-     inputt#reset
+     inputt#reset ;
+     ProofEngine.intros ~mk_fresh_name_callback () ;
+     refresh_sequent notebook ;
+     refresh_proof output
   with
      RefreshSequentException e ->
       output_html outputhtml
@@ -2138,7 +2157,7 @@ let call_tactic_with_hypothesis_input tactic () =
 ;;
 
 
-let intros = call_tactic ProofEngine.intros;;
+let intros = call_tactic (ProofEngine.intros ~mk_fresh_name_callback);;
 let exact = call_tactic_with_input ProofEngine.exact;;
 let apply = call_tactic_with_input ProofEngine.apply;;
 let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;;
@@ -2149,9 +2168,9 @@ let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
 let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
 let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
 let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
-let cut = call_tactic_with_input ProofEngine.cut;;
+let cut = call_tactic_with_input (ProofEngine.cut ~mk_fresh_name_callback);;
 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
-let letin = call_tactic_with_input ProofEngine.letin;;
+let letin = call_tactic_with_input (ProofEngine.letin ~mk_fresh_name_callback);;
 let ring = call_tactic ProofEngine.ring;;
 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;