* New button "Select only constants" to choose the URIs to try during the

  disambiguation phase. Usually the number of constants is small and among
  them there is the right URI.
* New ElimIntrosSimpl replaces the old ElimSimplIntros.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 2e9c702dcef5724c8402f0410acd4133595bcf9d..60d0d344b53b8c913a93efd420dcea9418cdf8f2 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -319,10 +319,12 @@ prerr_endline ("### " ^ CicPp.ppterm expr) ;
 exception NoChoice;;
 
 let
- interactive_user_uri_choice ~selection_mode ?(ok="Ok") ~title ~msg uris
+ interactive_user_uri_choice ~selection_mode ?(ok="Ok")
+  ?(enable_button_for_non_vars=false) ~title ~msg uris
 =
  let choices = ref [] in
  let chosen = ref false in
+ let use_only_constants = ref false in
  let window =
   GWindow.dialog ~modal:true ~title ~width:600 () in
  let lMessage =
@@ -352,6 +354,13 @@ let
   GButton.button ~label:ok
    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
  let _ = okb#misc#set_sensitive false in
+ let nonvarsb =
+  GButton.button
+   ~packing:
+    (function w ->
+      if enable_button_for_non_vars then
+       hbox#pack ~expand:false ~fill:false ~padding:5 w)
+   ~label:"Try constants only" () in
  let checkb =
   GButton.button ~label:"Check"
    ~packing:(hbox#pack ~padding:5) () in
@@ -368,6 +377,13 @@ let
   ignore (cancelb#connect#clicked window#destroy) ;
   ignore
    (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
+  ignore
+   (nonvarsb#connect#clicked
+     (function () ->
+       use_only_constants := true ;
+       chosen := true ;
+       window#destroy ()
+   )) ;
   ignore (checkb#connect#clicked check_callback) ;
   ignore
    (clist#connect#select_row
@@ -401,8 +417,13 @@ let
   window#set_position `CENTER ;
   window#show () ;
   GMain.Main.main () ;
-  if !chosen && List.length !choices > 0 then
-   !choices
+  if !chosen then
+   if !use_only_constants then
+    List.filter
+     (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
+     uris
+   else
+    if List.length !choices > 0 then !choices else raise NoChoice
   else
    raise NoChoice
 ;;
@@ -1335,6 +1356,7 @@ let locate_one_id id =
       interactive_user_uri_choice
        ~selection_mode:`EXTENDED
        ~ok:"Try every selection."
+       ~enable_button_for_non_vars:true
        ~title:"Ambiguous input."
        ~msg:
          ("Ambiguous input \"" ^ id ^
@@ -2274,7 +2296,7 @@ let call_tactic_with_hypothesis_input tactic () =
 let intros = call_tactic ProofEngine.intros;;
 let exact = call_tactic_with_input ProofEngine.exact;;
 let apply = call_tactic_with_input ProofEngine.apply;;
-let elimsimplintros = call_tactic_with_input ProofEngine.elim_simpl_intros;;
+let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;;
 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
 let whd = call_tactic_with_goal_input ProofEngine.whd;;
 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
@@ -3070,8 +3092,8 @@ object(self)
    let applyb =
     GButton.button ~label:"Apply"
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
-   let elimsimplintrosb =
-    GButton.button ~label:"ElimSimplIntros"
+   let elimintrossimplb =
+    GButton.button ~label:"ElimIntrosSimpl"
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
    let elimtypeb =
     GButton.button ~label:"ElimType"
@@ -3163,7 +3185,7 @@ object(self)
 
    ignore(exactb#connect#clicked exact) ;
    ignore(applyb#connect#clicked apply) ;
-   ignore(elimsimplintrosb#connect#clicked elimsimplintros) ;
+   ignore(elimintrossimplb#connect#clicked elimintrossimpl) ;
    ignore(elimtypeb#connect#clicked elimtype) ;
    ignore(whdb#connect#clicked whd) ;
    ignore(reduceb#connect#clicked reduce) ;