** Efficacité, bugs, robustesse CoqIDE **

- Suppression d'une source de fuite mémoire dans declare_mod.ml (la
  table de hash library_table n'était pas synchronisée avec le reset
  et elle grossissait à chaque rejeu de la session; utilisation au
  passage d'une map pour que la synchronisation avec le reset soit
  plus rapide). [mod_typing.ml]

- Correction d'un bug de synchronisation pour le niveau pattern 200.
  [pcoq.ml4]

- Suppression d'un vieux reste du traducteur [constructeur VernacVar]

- Robustesse et uniformité accrue dans CoqIDE vis à vis du statut de
  chacune des commandes vernaculaires par l'utilisation d'une fonction
  d'assignation d'attributs à chaque commande vernac.

  Correction de ce qui semble être des bizarreries
  (VernacDeclareTacticDefinition considéré comme ouvrant un but;
  suppression des "loc" dans les Reset: ne pouvait pas faire
  fonctionner correctement update_on_end_of_segment).

  Suppression de la nécessité d'expliciter si une commande retourne
  des messages dépendants du mode "verbose" (on suppose que chaque
  commande sait ce qu'elle doit dire selon la position du flag verbose).

  Sinon, le mécanisme de Reset de CoqIDE reste pauvre. CoqIDE ne
  sait revenir qu'aux états associés à des noms et cela ne vaut pas
  l'approche de Proof General. Il sera sans doute opportun de se
  brancher sur l'architecture de Pierre Courtieu à base de "Backtrack".

  La restriction des buts imbriqués a-t-elle vraiment une raison
  d'être ? En plus les commandes non cablées en dur comme Next
  Obligation ne sont pas prises en compte.

  Interdiction, dès Coq, d'ouvrir sections ou modules si preuve en cours.

  Réparation approximative de l'option "Help for Keyword" de Coqide
  mais encore à faire pour plus de robustesse (makefile, installation,
  synchronisation entre la version du fichier index_urls.txt et la
  version du refman, ...).



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

7 files changed, 269 insertions, 701 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index e75f507210..aef993be65 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -110,6 +110,166 @@ let is_in_proof_mode () =
 let user_error_loc l s =
   raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s)))
 
+type command_attribute =
+    NavigationCommand | QueryCommand | DebugCommand
+  | OtherStatePreservingCommand | GoalStartingCommand
+
+let rec attribute_of_vernac_command = function
+  (* Control *)
+  | VernacTime com -> attribute_of_vernac_command com
+  | VernacList _ -> [] (* unsupported *)
+  | VernacLoad _ -> []
+
+  (* Syntax *)
+  | VernacTacticNotation _ -> []
+  | VernacSyntaxExtension _ -> []
+  | VernacDelimiters _ -> []
+  | VernacBindScope _ -> []
+  | VernacOpenCloseScope _ -> []
+  | VernacArgumentsScope _ -> []
+  | VernacInfix _ -> []
+  | VernacNotation _ -> []
+
+  (* Gallina *)
+  | VernacDefinition (_,_,DefineBody _,_) -> []
+  | VernacDefinition (_,_,ProveBody _,_) -> [GoalStartingCommand]
+  | VernacStartTheoremProof _ -> [GoalStartingCommand]
+  | VernacEndProof _ -> []
+  | VernacExactProof _ -> []
+
+  | VernacAssumption _ -> []
+  | VernacInductive _ -> []
+  | VernacFixpoint _ -> []
+  | VernacCoFixpoint _ -> []
+  | VernacScheme _ -> []
+  | VernacCombinedScheme _ -> []
+
+  (* Modules *)
+  | VernacDeclareModule _ -> []
+  | VernacDefineModule _  -> []
+  | VernacDeclareModuleType _ -> []
+  | VernacInclude _ -> []
+
+  (* Gallina extensions *)
+  | VernacBeginSection _ -> []
+  | VernacEndSegment _ -> []
+  | VernacRecord _ -> []
+  | VernacRequire _ -> []
+  | VernacImport _ -> []
+  | VernacCanonical _ -> []
+  | VernacCoercion _ -> []
+  | VernacIdentityCoercion _ -> []
+
+  (* Type classes *)
+  | VernacClass _ -> []
+  | VernacInstance _ -> []
+  | VernacContext _ -> []
+  | VernacDeclareInstance _ -> []
+
+  (* Solving *)
+  | VernacSolve _ -> []
+  | VernacSolveExistential _ -> []
+
+  (* MMode *)
+  | VernacDeclProof -> []
+  | VernacReturn -> []
+  | VernacProofInstr _ -> []
+
+  (* Auxiliary file and library management *)
+  | VernacRequireFrom _ -> []
+  | VernacAddLoadPath _ -> []
+  | VernacRemoveLoadPath _ -> []
+  | VernacAddMLPath _ -> []
+  | VernacDeclareMLModule _ -> []
+  | VernacChdir _ -> [OtherStatePreservingCommand]
+
+  (* State management *)
+  | VernacWriteState _ -> []
+  | VernacRestoreState _ -> []
+
+  (* Resetting *)
+  | VernacRemoveName _ -> [NavigationCommand]
+  | VernacResetName _ -> [NavigationCommand]
+  | VernacResetInitial -> [NavigationCommand]
+  | VernacBack _ -> [NavigationCommand]
+  | VernacBackTo _ -> [NavigationCommand]
+
+  (* Commands *)
+  | VernacDeclareTacticDefinition _ -> []
+  | VernacHints _ -> []
+  | VernacSyntacticDefinition _ -> []
+  | VernacDeclareImplicits _ -> []
+  | VernacReserve _ -> []
+  | VernacSetOpacity _ -> []
+  | VernacSetOption (Goptions.SecondaryTable ("Ltac","Debug"), _) -> 
+      [DebugCommand]
+  | VernacSetOption _ -> []
+  | VernacUnsetOption _ -> []
+  | VernacRemoveOption _ -> []
+  | VernacAddOption _ -> []
+  | VernacMemOption _ -> [QueryCommand]
+
+  | VernacPrintOption _ -> [QueryCommand]
+  | VernacCheckMayEval _ -> [QueryCommand]
+  | VernacGlobalCheck _ -> [QueryCommand]
+  | VernacPrint _ -> [QueryCommand]
+  | VernacSearch _ -> [QueryCommand]
+  | VernacLocate _ -> [QueryCommand]
+
+  | VernacComments _ -> [OtherStatePreservingCommand]
+  | VernacNop -> [OtherStatePreservingCommand]
+
+  (* Proof management *)
+  | VernacGoal _ -> [GoalStartingCommand]
+
+  | VernacAbort _ -> [NavigationCommand]
+  | VernacAbortAll -> [NavigationCommand]
+  | VernacRestart -> [NavigationCommand]
+  | VernacSuspend -> [NavigationCommand]
+  | VernacResume _ -> [NavigationCommand]
+  | VernacUndo _ -> [NavigationCommand]
+  | VernacUndoTo _ -> [NavigationCommand]
+  | VernacBacktrack _ -> [NavigationCommand]
+
+  | VernacFocus _ -> []
+  | VernacUnfocus -> []
+  | VernacGo _ -> []
+  | VernacShow _ -> [OtherStatePreservingCommand]
+  | VernacCheckGuard -> [OtherStatePreservingCommand]
+  | VernacProof (Tacexpr.TacId []) -> [OtherStatePreservingCommand]
+  | VernacProof _ -> []
+
+  (* Toplevel control *)
+  | VernacToplevelControl _ -> []
+
+  (* Extensions *)
+  | VernacExtend _ -> []
+
+let is_vernac_goal_starting_command com =
+  List.mem GoalStartingCommand (attribute_of_vernac_command com)
+
+let is_vernac_navigation_command com =
+  List.mem NavigationCommand (attribute_of_vernac_command com)
+
+let is_vernac_query_command com =
+  List.mem QueryCommand (attribute_of_vernac_command com)
+
+let is_vernac_debug_command com =
+  List.mem DebugCommand (attribute_of_vernac_command com)
+
+let is_vernac_state_preserving_command com =
+  let attribute = attribute_of_vernac_command com in
+  let b =
+    List.mem OtherStatePreservingCommand attribute or
+    List.mem QueryCommand attribute in
+  if b then prerr_endline "state preserving command found";
+  b
+
+let rec is_tactic = function
+  | VernacSolve _ -> true
+  | VernacTime com -> is_tactic com
+  | _ -> false
+
 let interp verbosely s = 
   prerr_endline "Starting interp...";
   prerr_endline s;
@@ -118,51 +278,20 @@ let interp verbosely s =
   match pe with 
     | None -> assert false
     | Some((loc,vernac) as last) ->
-	match vernac with
-	  | VernacDefinition _  | VernacStartTheoremProof _ 
-	  | VernacBeginSection _ | VernacGoal _
-	  | VernacDefineModule _ | VernacDeclareModuleType _
-	  | VernacDeclareTacticDefinition _
-		when is_in_proof_mode () -> 
-		  user_error_loc loc (str "CoqIDE do not support nested goals")
-	  | VernacSetOption (Goptions.SecondaryTable ("Ltac","Debug"), _) ->
-	      user_error_loc loc (str "Debug mode not available within CoqIDE")
-	  | VernacResetName _
-	  | VernacResetInitial 
-	  | VernacBack _ 
-	  | VernacAbort _ 
-	  | VernacAbortAll
-	  | VernacRestart
-	  | VernacSuspend
-	  | VernacResume _
-	  | VernacUndo _ ->
-	      user_error_loc loc (str "Use CoqIDE navigation instead") 
-	  | _ ->
-	      begin
-		match vernac with
-		  | VernacPrintOption _ 
-		  | VernacCheckMayEval _
-		  | VernacGlobalCheck _
-		  | VernacPrint _
-		  | VernacSearch _ 
-		    -> !flash_info 
-			"Warning: query commands should not be inserted in scripts" 
-		  | VernacDefinition (_,_,DefineBody _,_) 
-		  | VernacInductive _
-		  | VernacFixpoint _
-		  | VernacCoFixpoint _
-		  | VernacEndProof _
-                  | VernacScheme _ 
-		  | VernacExtend("Extraction", _)
-		  | VernacExtend("ExtractionLibrary",_)
-		  | VernacExtend("RecursiveExtractionLibrary",_)
-		    -> Flags.make_silent (not verbosely)
-		  | _ -> ()
-	      end;
-	      Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s));
-	      Flags.make_silent true;
-	      prerr_endline ("...Done with interp of : "^s);
-	      last
+	if is_vernac_goal_starting_command vernac & is_in_proof_mode () then
+	  user_error_loc loc (str "CoqIDE do not support nested goals");
+	if is_vernac_debug_command vernac then
+	  user_error_loc loc (str "Debug mode not available within CoqIDE");
+	if is_vernac_navigation_command vernac then
+	  user_error_loc loc (str "Use CoqIDE navigation instead");
+	if is_vernac_query_command vernac then 
+	  !flash_info
+	    "Warning: query commands should not be inserted in scripts";
+	Flags.make_silent (not verbosely); (*verbose if in small step forward*)
+	Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s));
+	Flags.make_silent true;
+	prerr_endline ("...Done with interp of : "^s);
+	last
 
 let interp_and_replace s = 
   let result = interp false s in
@@ -199,11 +328,6 @@ let try_interptac s =
   | Stdpp.Exc_located (_,e) -> prerr_endline ("try_interp: failed ("^(Printexc.to_string e)); Failed
   | e -> Failed	  
 
-let is_tactic = function
-  | VernacSolve _ -> true
-  | _ -> false
-
-
 let rec is_pervasive_exn = function
   | Out_of_memory | Stack_overflow | Sys.Break -> true
   | Error_in_file (_,_,e) -> is_pervasive_exn e
@@ -339,20 +463,24 @@ let word_class s =
     SHashtbl.find word_tbl s
   with Not_found -> Normal
 
-type reset_info = NoReset | Reset of Names.identifier * bool ref
+type reset_info =
+  | NoReset
+  | ResetAtDecl of Names.identifier * bool ref 
+  | ResetAtSegmentStart of Names.identifier * bool ref
 
 let compute_reset_info = function 
-  | VernacDefinition (_, (_,id), DefineBody _, _) 
-  | VernacBeginSection (_,id) 
-  | VernacDefineModule (_,(_,id), _, _, _) 
-  | VernacDeclareModule (_,(_,id), _, _)
-  | VernacDeclareModuleType ((_,id), _, _)
+  | VernacBeginSection id 
+  | VernacDefineModule (_,id, _, _, _) 
+  | VernacDeclareModule (_,id, _, _)
+  | VernacDeclareModuleType (id, _, _) ->
+      ResetAtSegmentStart (snd id, ref true)
+  | VernacDefinition (_, (_,id), DefineBody _, _)
   | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
   | VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
-      Reset (id, ref true)
+      ResetAtDecl (id, ref true)
   | VernacDefinition (_, (_,id), ProveBody _, _)
   | VernacStartTheoremProof (_, [Some (_,id), _], _, _) ->
-      Reset (id, ref false)
+      ResetAtDecl (id, ref false)
   | _ -> NoReset
 
 let reset_initial () = 
@@ -472,16 +600,6 @@ let make_cases s =
 	  []
     | _ -> raise Not_found
 
-let is_state_preserving = function
-  | VernacPrint _ | VernacPrintOption _ | VernacGlobalCheck _
-  | VernacCheckMayEval _ | VernacSearch _ | VernacLocate _ 
-  | VernacShow _ | VernacMemOption _ | VernacComments _ 
-  | VernacChdir None | VernacNop -> 
-      prerr_endline "state preserving command found"; true
-  | _ -> 
-      false
-
-
 let current_status () = 
   let path = msg (Libnames.pr_dirpath (Lib.cwd ())) in
   let path = if path = "Top" then "Ready" else "Ready in " ^ String.sub path 4 (String.length path - 4) in
diff --git a/ide/coq.mli b/ide/coq.mli
index 991f104dbe..32a62c2306 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -21,7 +21,8 @@ val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit
 val interp_and_replace : string -> (Util.loc * Vernacexpr.vernac_expr) * string
 
 val is_tactic : Vernacexpr.vernac_expr -> bool
-val is_state_preserving : Vernacexpr.vernac_expr -> bool
+val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool
+val is_vernac_goal_starting_command : Vernacexpr.vernac_expr -> bool
 
 (* type hyp = (identifier * constr option * constr) * string *)
 
@@ -41,7 +42,10 @@ val print_no_goal : unit -> string
 
 val process_exn : exn -> string*(Util.loc option)
 
-type reset_info = NoReset | Reset of Names.identifier * bool ref
+type reset_info =
+  | NoReset
+  | ResetAtDecl of Names.identifier * bool ref 
+  | ResetAtSegmentStart of Names.identifier * bool ref
 
 val compute_reset_info : Vernacexpr.vernac_expr -> reset_info
 val reset_initial : unit -> unit
diff --git a/ide/coqide.ml b/ide/coqide.ml
index f223972df6..29b55da6aa 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -459,7 +459,7 @@ let rec complete input_buffer w (offset:int) =
 	
 let get_current_word () =
   let av = Option.get ((get_current_view ()).analyzed_view) in 
-    match GtkBase.Clipboard.wait_for_text (cb ())#as_clipboard with
+    match (cb ())#text with
       | None -> 
 	  prerr_endline "None selected";
 	  let it = av#get_insert in
@@ -498,19 +498,16 @@ let pop () = try Stack.pop processed_stack with Stack.Empty -> raise (Size 0)
 let top () = try Stack.top processed_stack with Stack.Empty -> raise (Size 0)
 let is_empty () = Stack.is_empty processed_stack
 
-  
 (* push a new Coq phrase *)
 
-let update_on_end_of_proof id =
+let update_on_end_of_proof () =
   let lookup_lemma = function
-    | { ast = _, ( VernacDefinition (_, _, ProveBody _, _)
-	| VernacDeclareTacticDefinition _
-	| VernacStartTheoremProof _) ; 
-	reset_info = Reset (_, r) } -> 
-	if not !r then begin 
+    | { reset_info = ResetAtDecl (_, r) } ->
+	if not !r then begin
 	    prerr_endline "Toggling Reset info to true";
 	    r := true; raise Exit end
 	else begin
+	  (* Hide the Definition done since last started proof *)
 	    prerr_endline "Toggling Changing Reset id"; 
 	    r := false
 	  end
@@ -521,13 +518,9 @@ let update_on_end_of_proof id =
 
 let update_on_end_of_segment id =
   let lookup_section = function 
-    | { ast = _, ( VernacBeginSection id'
-	| VernacDefineModule (_,id',_,_,None)
-	| VernacDeclareModule (_,id',_,_)
-	| VernacDeclareModuleType (id',_,None)); 
-	reset_info = Reset (_, r) } 
-	when id = id' -> raise Exit
-    | { reset_info = Reset (_, r) } -> r := false
+    | { reset_info = ResetAtSegmentStart (id', r) } when id = id' -> raise Exit
+    | { reset_info = ResetAtSegmentStart (_, r) } -> r := false
+    | { reset_info = ResetAtDecl (_, r) } -> r := false
     | _ -> ()
   in
     try Stack.iter lookup_section processed_stack with Exit -> ()
@@ -537,21 +530,26 @@ let push_phrase start_of_phrase_mark end_of_phrase_mark ast =
 	   stop = end_of_phrase_mark;
 	   ast = ast;
 	   reset_info = Coq.compute_reset_info (snd ast)
-	  } 
-  in
-    push x;
+	  } in
+  begin
     match snd ast with
       | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof ()
-      | VernacEndSegment id -> update_on_end_of_segment id
+      | VernacEndSegment (_,id) -> update_on_end_of_segment id
       | _ -> ()
+  end;
+  push x
+
 
 let repush_phrase x =
   let x = { x with reset_info = Coq.compute_reset_info (snd x.ast) } in
-    push x;
+  begin
     match snd x.ast with
       | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof ()
-      | VernacEndSegment id -> update_on_end_of_segment id
+      | VernacEndSegment (_,id) -> update_on_end_of_segment id
       | _ -> ()
+  end;
+  push x
+
 
 (* For electric handlers *)
 exception Found
@@ -1284,13 +1282,10 @@ object(self)
       else begin
 	  let t = pop () in
 	    begin match t.reset_info with
-	      | Reset (id, ({contents=true} as v)) -> v:=false; 
-		  (match snd t.ast with
-		     | VernacBeginSection _ | VernacDefineModule _ 
-		     | VernacDeclareModule _ | VernacDeclareModuleType _
-		     | VernacEndSegment _ 
-		       -> reset_to_mod id
-		     | _ ->  reset_to id)
+	      | ResetAtSegmentStart (id, ({contents=true} as v)) ->
+		  v:=false; reset_to_mod id
+	      | ResetAtDecl (id, ({contents=true} as v)) ->
+		  v:=false; reset_to id
 	      | _ -> synchro ()
 	    end;
 	    interp_last t.ast;
@@ -1388,20 +1383,16 @@ Please restart and report NOW.";
 		      try Pfedit.undo 1; ignore (pop ()); sync update_input () 
 		      with _ -> self#backtrack_to_no_lock start
 		    end
-		| {ast=_,t;reset_info=Reset (id, {contents=true})} ->
+
+		| {reset_info=ResetAtSegmentStart (id, {contents=true})} ->
+		    ignore (pop ());
+		    reset_to_mod id;
+		    sync update_input ()
+		| {reset_info=ResetAtDecl (id, {contents=true})} ->
 		    ignore (pop ());
-		    (match t with 
-		       | VernacBeginSection _ | VernacDefineModule _ 
-		       | VernacDeclareModule _ | VernacDeclareModuleType _
-		       | VernacEndSegment _
-			 -> reset_to_mod id
-		       | _ ->  reset_to id);
+		    reset_to id;
 		    sync update_input ()
-		| { ast = _, ( VernacStartTheoremProof _ 
-		    | VernacGoal _
-		    | VernacDeclareTacticDefinition _
-		    | VernacDefinition (_,_,ProveBody _,_));
-		    reset_info=Reset(id,{contents=false})} ->
+		| {reset_info=ResetAtDecl (id,{contents=false})} ->
 		    ignore (pop ());
 		    (try 
 			 Pfedit.delete_current_proof () 
@@ -1411,7 +1402,7 @@ Please restart and report NOW.";
 			 raise e
 		       end);
 		    sync update_input ()
-		| { ast = (_, a) } when is_state_preserving a ->
+		| { ast = (_, a) } when is_vernac_state_preserving_command a ->
 		    ignore (pop ());
 		    sync update_input ()
 		| _ -> 
@@ -2418,8 +2409,8 @@ let main files =
 				       | None -> ()
 				       | Some f ->
 					   save_f ();
-					   let l,r = !current.cmd_editor in
-					   let _ = run_command av#insert_message (l ^ (Filename.quote f) ^ r) in
+					   let com = Flags.subst_command_placeholder !current.cmd_editor (Filename.quote f) in
+					   let _ = run_command av#insert_message com in
 					     av#revert)
 			    in
 			    let _ = edit_f#add_separator () in
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index b79e4b9361..f4fd73d6fd 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -268,9 +268,11 @@ let run_command f c =
   (Unix.close_process_full (cin,cout,cerr),  Buffer.contents result)
 
 let browse f url =
-  let l,r = !current.cmd_browse in
-  let (_s,_res) = run_command f (l ^ url ^ r) in
-  ()
+  let com = Flags.subst_command_placeholder !current.cmd_browse url in
+  let (s,_res) = run_command f com in
+  if s = Unix.WEXITED 127 then
+    prerr_endline
+      ("Could not execute\n  \""^com^"\"\ncheck your preferences for setting a valid browser command")
 
 let url_for_keyword =
   let ht = Hashtbl.create 97 in
@@ -295,7 +297,8 @@ let url_for_keyword =
 
 let browse_keyword f text = 
   try let u = url_for_keyword text in browse f (!current.doc_url ^ u) 
-  with _ -> ()
+  with Not_found ->
+    prerr_endline ("No documentation found for "^text)
 
 
 let underscore = Glib.Utf8.to_unichar "_" (ref 0)
diff --git a/ide/index_urls.txt b/ide/index_urls.txt
deleted file mode 100644
index fea61809df..0000000000
--- a/ide/index_urls.txt
+++ /dev/null
@@ -1,563 +0,0 @@
-+,node.0.2.0.html#@default146
--,node.0.2.1.html#@default247
-2,node.1.2.9.html#@default514
-;,node.1.2.12.html#@default547
-?,node.1.0.6.html#@default358
-?,node.1.2.1.html#@default410
-&,node.0.2.0.html#@default164
-{A}+{B},node.0.2.0.html#@default174
-{x:A & (P x)},node.0.2.0.html#@default163
-{x:A | (P x)},node.0.2.0.html#@default157
-|,node.0.2.0.html#@default158
-A*B,node.0.2.0.html#@default150
-A+{B},node.0.2.0.html#@default178
-A+B,node.0.2.0.html#@default145
-Abort,node.1.1.0.html#@default385
-Absolute names,node.0.1.6.html#@default85
-Abstract,node.1.2.12.html#@default559
-Absurd,node.1.2.3.html#@default442
-Acc,node.0.2.0.html#@default215
-Acc_inv,node.0.2.0.html#@default216
-Acc_rec,node.0.2.0.html#@default217
-Add Abstract Ring,node.3.7.4.html#@default643
-Add Abstract Semi Ring,node.3.7.4.html#@default644
-Add Field,node.1.2.10.html#@default526
-Add LoadPath,node.1.0.4.html#@default338
-Add ML Path,node.1.0.4.html#@default342
-Add Morphism,node.3.8.2.html#@default647
-Add Printing If,node.0.1.1.html#@default67
-Add Printing Let,node.0.1.1.html#@default63
-Add Rec LoadPath,node.1.0.4.html#@default339
-Add Rec ML Path,node.1.0.4.html#@default343
-Add Ring,node.1.2.10.html#@default523
-Add Semi Ring,node.1.2.10.html#@default524
-Add Setoid,node.3.8.1.html#@default646
-All,node.0.2.0.html#@default110
-AllT,node.0.2.0.html#@default224
-Apply,node.1.2.2.html#@default427
-Apply ... with,node.1.2.2.html#@default428
-Arithmetical notations,node.0.2.1.html#@default244
-Arity,node.0.3.4.html#@default288
-Assert,node.1.2.2.html#@default433
-Associativity,node.2.0.1.html#@default571
-Assumption,node.1.2.2.html#@default412
-Auto,node.1.2.10.html#@default515
-AutoRewrite,node.1.2.10.html#@default528
-Axiom,node.0.0.2.html#@default24
-abstractions,node.0.0.1.html#@default16
-absurd,node.0.2.0.html#@default121
-absurd_set,node.0.2.0.html#@default188
-all,node.0.2.0.html#@default109
-allT,node.0.2.0.html#@default223
-and,node.0.2.0.html#@default99
-and_rec,node.0.2.0.html#@default189
-applications,node.0.0.1.html#@default18
-Back,node.1.0.5.html#@default348
-Bad Magic Number,node.1.0.3.html#@default331
-Begin Silent,node.1.0.7.html#@default366
-Binding list,node.1.2.2.html#@default441
-beta-reduction,node.0.3.2.html#@default274
-bool,node.0.2.0.html#@default135
-bool_choice,node.0.2.0.html#@default181
-byte-code,node.3.0.0.html#@default574
-Calculus of (Co)Inductive Constructions,node.0.3.html#@default255
-Canonical Structure,node.0.1.7.html#@default91
-Case,node.1.2.6.html#@default468
-Case ... with,node.1.2.6.html#@default469
-Cases,node.3.2.html#@default593
-Cases...of...end,node.0.0.1.html#@default21
-Cbv,node.1.2.4.html#@default445
-Cd,node.1.0.4.html#@default337
-Change,node.1.2.2.html#@default438
-Change ... in,node.1.2.2.html#@default440
-Chapter,node.0.1.3.html#@default73
-Check,node.1.0.1.html#@default308
-Choice,node.0.2.0.html#@default179
-Choice2,node.0.2.0.html#@default180
-CIC,node.0.3.html#@default254
-Clear,node.1.2.2.html#@default414
-ClearBody,node.1.2.2.html#@default415
-Coercion,node.3.3.5.html#@default601
-Coercion Local,node.3.3.5.html#@default602
-Coercions,node.0.1.8.html#@default92
-and sections,node.3.3.9.html#@default616
-classes,node.3.3.1.html#@default596
-FUNCLASS,node.3.3.2.html#@default597
-identity,node.3.3.3.html#@default599
-inheritance graph,node.3.3.4.html#@default600
-presentation,node.3.3.html#@default595
-SORTCLASS,node.3.3.2.html#@default598
-CoFixpoint,node.0.0.2.html#@default40
-CoInductive,node.0.0.2.html#@default38
-Comments,node.0.0.0.html#@default2
-Compare,node.1.2.8.html#@default489
-Compiled files,node.1.0.3.html#@default327
-Compute,node.1.2.4.html#@default447
-Connectives,node.0.2.0.html#@default94
-Constant,node.0.0.2.html#@default31
-Constructor,node.1.2.5.html#@default455
-Constructor ...  with,node.1.2.5.html#@default456
-Context,node.0.3.1.html#@default263
-Contradiction,node.1.2.3.html#@default443
-Contributions,node.0.2.2.html#@default253
-Conversion rules,node.0.3.2.html#@default273
-Conversion tactics,node.1.2.4.html#@default444
-coqdep,node.3.1.1.html#@default582
-coq_Makefile,node.3.1.2.html#@default584
-coqmktop,node.3.1.0.html#@default579
-coq-tex,node.3.1.3.html#@default586
-coqweb,node.3.1.3.html#@default587
-Correctness,node.3.5.html#@default619
-Cut,node.1.2.2.html#@default434
-CutRewrite,node.1.2.7.html#@default482
-congr_eqT,node.0.2.0.html#@default241
-conj,node.0.2.0.html#@default100
-coqc,node.3.0.html#@default573
-coqtop,node.3.0.html#@default572
-Datatypes,node.0.2.0.html#@default132
-Debugger,node.3.1.0.html#@default580
-Decide Equality,node.1.2.8.html#@default488
-Declarations,node.0.0.2.html#@default23
-Declare ML Module,node.1.0.3.html#@default333
-Decompose,node.1.2.6.html#@default473
-Decompose Record,node.1.2.6.html#@default475
-Decompose Sum,node.1.2.6.html#@default474
-Defined,node.0.0.2.html#@default48
-Definition,node.0.0.2.html#@default33
-Definitions,node.0.0.2.html#@default29
-Dependencies,node.3.1.1.html#@default581
-Dependent Inversion,node.1.2.9.html#@default501
-Dependent Inversion ... with,node.1.2.9.html#@default503
-Dependent Inversion_clear,node.1.2.9.html#@default502
-Dependent Inversion_clear ... with,node.1.2.9.html#@default504
-Dependent Rewrite ->,node.1.2.8.html#@default495
-Dependent Rewrite <-,node.1.2.8.html#@default496
-Derive Dependent Inversion,node.1.2.9.html#@default511
-Derive Dependent Inversion_clear,node.1.2.9.html#@default512
-Derive Inversion,node.1.2.9.html#@default508
-Derive Inversion_clear,node.1.2.9.html#@default509
-Derive Inversion_clear ... with,node.1.2.9.html#@default510
-Destruct,node.1.2.6.html#@default466
-Discriminate,node.1.2.8.html#@default490
-DiscrR,node.0.2.1.html#@default250
-Do,node.1.2.12.html#@default542
-Double Induction,node.1.2.6.html#@default472
-Drop,node.1.0.7.html#@default365
-delta-reduction,node.0.0.2.html#@default30
-EApply,node.1.2.2.html#@default429
-EAuto,node.1.2.10.html#@default517
-Elim ... using,node.1.2.6.html#@default463
-Elim ... with,node.1.2.6.html#@default462
-Singleton elimination,node.0.3.4.html#@default294
-Elimination sorts,node.0.3.4.html#@default291
-ElimType,node.1.2.6.html#@default464
-Emacs,node.3.1.5.html#@default589
-EmptyT,node.0.2.0.html#@default233
-End,node.0.1.3.html#@default74
-End Silent,node.1.0.7.html#@default368
-Environment,node.0.0.2.html#@default32
-Environment variables,node.3.0.3.html#@default577
-Equality,node.0.2.0.html#@default118
-Eval,node.1.0.1.html#@default309
-EX,node.0.2.0.html#@default113
-EXT,node.0.2.0.html#@default229
-Ex,node.0.2.0.html#@default112
-Ex2,node.0.2.0.html#@default116
-Exact,node.1.2.1.html#@default408
-Exc,node.0.2.0.html#@default182
-Except,node.0.2.0.html#@default187
-Exists,node.1.2.5.html#@default458
-Explicitation of implicit arguments,node.0.1.7.html#@default88
-ExT,node.0.2.0.html#@default228
-ExT2,node.0.2.0.html#@default231
-Extensive grammars,node.1.0.6.html#@default362
-Extract Constant,node.3.6.1.html#@default637
-Extract Inductive,node.3.6.1.html#@default638
-Extraction,node.3.6.html#@default623
-Extraction,node.1.0.1.html#@default310
-Extraction Inline,node.3.6.1.html#@default633
-Extraction Language,node.3.6.1.html#@default628
-Extraction Module,node.3.6.0.html#@default626
-Extraction NoInline,node.3.6.1.html#@default634
-eq,node.0.2.0.html#@default119
-eq_add_S,node.0.2.0.html#@default193
-eq_ind_r,node.0.2.0.html#@default126
-eq_rec,node.0.2.0.html#@default186
-eq_rec_r,node.0.2.0.html#@default127
-eq_rect,node.0.2.0.html#@default128
-eq_rect_r,node.0.2.0.html#@default129
-eq_S,node.0.2.0.html#@default190
-eqT,node.0.2.0.html#@default236
-eqT_ind_r,node.0.2.0.html#@default242
-eqT_rec_r,node.0.2.0.html#@default243
-error,node.0.2.0.html#@default184
-ex,node.0.2.0.html#@default111
-ex2,node.0.2.0.html#@default115
-ex_intro,node.0.2.0.html#@default114
-ex_intro2,node.0.2.0.html#@default117
-exist,node.0.2.0.html#@default160
-exist2,node.0.2.0.html#@default162
-existS,node.0.2.0.html#@default166
-existS2,node.0.2.0.html#@default170
-exT,node.0.2.0.html#@default227
-exT2,node.0.2.0.html#@default232
-exT_intro,node.0.2.0.html#@default230
-Fact,node.0.0.2.html#@default44
-Fail,node.1.2.12.html#@default540
-False,node.0.2.0.html#@default97
-False_rec,node.0.2.0.html#@default185
-Field,node.1.2.10.html#@default525
-First,node.1.2.12.html#@default553
-Fix,node.0.3.4.html#@default298
-Fix_F,node.0.2.0.html#@default219
-Fix_F_eq,node.0.2.0.html#@default222
-Fix_F_inv,node.0.2.0.html#@default221
-Fixpoint,node.0.0.2.html#@default39
-Focus,node.1.1.1.html#@default392
-Fold,node.1.2.4.html#@default453
-Fourier,node.1.2.10.html#@default527
-Fst,node.0.2.0.html#@default155
-f_equal,node.0.2.0.html#@default124
-f_equal<I>i</I>,node.0.2.0.html#@default130
-false,node.0.2.0.html#@default137
-fix_eq,node.0.2.0.html#@default220
-fst,node.0.2.0.html#@default153
-Gallina,node.0.0.html#@default0
-gallina,node.3.1.6.html#@default591
-Generalize,node.1.2.2.html#@default436
-Generalize Dependent,node.1.2.2.html#@default437
-Global Variable,node.3.5.2.html#@default620
-Goal,node.0.0.2.html#@default50
-Grammar,node.1.0.6.html#@default361
-ge,node.0.2.0.html#@default208
-gen,node.0.2.0.html#@default226
-goal,node.1.2.html#@default405
-gt,node.0.2.0.html#@default209
-Head normal form,node.0.3.2.html#@default286
-Hint,node.1.2.11.html#@default531
-Hint Rewrite,node.1.2.10.html#@default529
-Hints databases,node.1.2.11.html#@default530
-Hints Immediate,node.1.2.11.html#@default533
-Hints Resolve,node.1.2.11.html#@default532
-Hints Unfold,node.1.2.11.html#@default534
-Hnf,node.1.2.4.html#@default449
-HTML,node.3.1.4.html#@default588
-Hypothesis,node.0.0.2.html#@default28
-I,node.0.2.0.html#@default96
-Identity Coercion,node.3.3.5.html#@default605
-Idtac,node.1.2.12.html#@default538
-IF,node.0.2.0.html#@default107
-proof of,node.3.5.html#@default618
-Implicit Arguments Off,node.1.0.6.html#@default355
-Implicit Arguments On,node.1.0.6.html#@default354
-Implicits,node.1.0.6.html#@default356
-Induction,node.1.2.6.html#@default465
-Inductive,node.0.0.2.html#@default36
-Inductive definitions,node.0.0.2.html#@default35
-Infix,node.1.0.6.html#@default363
-Info,node.1.2.12.html#@default557
-Injection,node.1.2.8.html#@default492
-Inspect,node.1.0.0.html#@default305
-Intro,node.1.2.2.html#@default418
-Intro ... after,node.1.2.2.html#@default426
-Intro after,node.1.2.2.html#@default425
-Intros,node.1.2.2.html#@default422
-Intros pattern,node.1.2.6.html#@default471
-Intros until,node.1.2.2.html#@default423
-Intuition,node.1.2.10.html#@default520
-Inversion,node.1.2.9.html#@default497
-Inversion ... in,node.1.2.9.html#@default499
-Inversion ... using,node.1.2.9.html#@default505
-Inversion ... using ... in,node.1.2.9.html#@default506
-Inversion_clear,node.1.2.9.html#@default498
-Inversion_clear ... in,node.1.2.9.html#@default500
-IsSucc,node.0.2.0.html#@default195
-if ... then ... else,node.0.1.1.html#@default55
-iff,node.0.2.0.html#@default106
-implicit arguments,node.0.1.7.html#@default86
-inl,node.0.2.0.html#@default147
-inleft,node.0.2.0.html#@default176
-inr,node.0.2.0.html#@default148
-inright,node.0.2.0.html#@default177
-iota-reduction,node.0.3.2.html#@default275
-LApply,node.1.2.2.html#@default430
-Lazy,node.1.2.4.html#@default446
-Left,node.1.2.5.html#@default459
-Lemma,node.0.0.2.html#@default42
-LetTac,node.1.2.2.html#@default431
-Lexical conventions,node.0.0.0.html#@default1
-Libraries,node.0.1.5.html#@default82
-Load,node.1.0.2.html#@default325
-Load Verbose,node.1.0.2.html#@default326
-Loadpath,node.1.0.4.html#@default335
-Local,node.0.0.2.html#@default34
-Local definitions,node.0.0.1.html#@default19
-Locate,node.1.0.1.html#@default323
-Locate Library,node.1.0.4.html#@default346
-Logical paths,node.0.1.5.html#@default83
-le,node.0.2.0.html#@default204
-le_n,node.0.2.0.html#@default205
-le_S,node.0.2.0.html#@default206
-left,node.0.2.0.html#@default172
-let ... in,node.0.1.1.html#@default56
-let-in,node.0.0.1.html#@default20
-local context,node.1.1.html#@default372
-lt,node.0.2.0.html#@default207
-Makefile,node.3.1.2.html#@default583
-Man pages,node.3.1.7.html#@default592
-ML-like patterns,node.0.1.1.html#@default54
-Module,node.0.1.4.html#@default75
-Module Type,node.0.1.4.html#@default78
-Move,node.1.2.2.html#@default416
-Mutual Inductive,node.0.0.2.html#@default37
-mult,node.0.2.0.html#@default201
-mult_n_O,node.0.2.0.html#@default202
-mult_n_Sm,node.0.2.0.html#@default203
-NewDestruct,node.1.2.6.html#@default467
-NewInduction,node.1.2.6.html#@default461
-None,node.0.2.0.html#@default143
-Normal form,node.0.3.2.html#@default285
-Notation,node.2.0.0.html#@default569
-Notations for real numbers,node.0.2.1.html#@default249
-n_Sn,node.0.2.0.html#@default197
-nat,node.0.2.0.html#@default138
-nat_case,node.0.2.0.html#@default210
-nat_double_ind,node.0.2.0.html#@default211
-native code,node.3.0.0.html#@default575
-not,node.0.2.0.html#@default98
-not_eq_S,node.0.2.0.html#@default194
-notT,node.0.2.0.html#@default235
-O,node.0.2.0.html#@default139
-O_S,node.0.2.0.html#@default196
-Omega,node.1.2.10.html#@default521
-Opaque,node.1.0.1.html#@default311
-Options of the command line,node.3.0.4.html#@default578
-Orelse,node.1.2.12.html#@default544
-option,node.0.2.0.html#@default141
-or,node.0.2.0.html#@default103
-or_introl,node.0.2.0.html#@default104
-or_intror,node.0.2.0.html#@default105
-Parameter,node.0.0.2.html#@default25
-Pattern,node.1.2.4.html#@default454
-Peano's arithmetic notations,node.0.2.1.html#@default248
-Pose,node.1.2.2.html#@default432
-Positivity,node.0.3.4.html#@default287
-Precedences,node.2.0.1.html#@default570
-Pretty printing,node.1.0.6.html#@default360
-Print,node.1.0.0.html#@default302
-Print All,node.1.0.0.html#@default304
-Print Classes,node.3.3.6.html#@default606
-Print Coercion Paths,node.3.3.6.html#@default609
-Print Coercions,node.3.3.6.html#@default607
-Print Extraction Inline,node.3.6.1.html#@default635
-Print Graph,node.3.3.6.html#@default608
-Print Hint,node.1.2.11.html#@default535
-Print HintDb,node.1.2.11.html#@default536
-Print LoadPath,node.1.0.4.html#@default341
-Print ML Modules,node.1.0.3.html#@default334
-Print ML Path,node.1.0.4.html#@default344
-Print Module,node.0.1.4.html#@default80
-Print Module Type,node.0.1.4.html#@default81
-Print Modules,node.1.0.3.html#@default332
-Print Proof,node.1.0.0.html#@default303
-Print Section,node.1.0.0.html#@default306
-Print Table Printing If,node.0.1.1.html#@default70
-Print Table Printing Let,node.0.1.1.html#@default66
-Programming,node.0.2.0.html#@default131
-Prolog,node.1.2.10.html#@default518
-Prompt,node.1.1.html#@default371
-Proof,node.0.0.2.html#@default45
-Proof editing,node.1.1.html#@default370
-Proof General,node.3.1.5.html#@default590
-Proof term,node.1.1.html#@default373
-Prop,node.0.0.1.html#@default11
-Pwd,node.1.0.4.html#@default336
-pair,node.0.2.0.html#@default152
-plus,node.0.2.0.html#@default198
-plus_n_O,node.0.2.0.html#@default199
-plus_n_Sm,node.0.2.0.html#@default200
-pred,node.0.2.0.html#@default191
-pred_Sn,node.0.2.0.html#@default192
-prod,node.0.2.0.html#@default149
-products,node.0.0.1.html#@default17
-proj1,node.0.2.0.html#@default101
-proj2,node.0.2.0.html#@default102
-projS1,node.0.2.0.html#@default167
-projS2,node.0.2.0.html#@default168
-Qed,node.0.0.2.html#@default47
-Qualified identifiers,node.0.1.6.html#@default84
-Quantifiers,node.0.2.0.html#@default108
-Quit,node.1.0.7.html#@default364
-Quote,node.1.2.9.html#@default513
-?,node.0.1.7.html#@default90
-Read Module,node.1.0.3.html#@default328
-Record,node.0.1.0.html#@default52
-Recursion,node.0.2.0.html#@default213
-Recursive arguments,node.0.3.4.html#@default300
-Recursive Extraction,node.3.6.0.html#@default625
-Recursive Extraction Module,node.3.6.0.html#@default627
-Red,node.1.2.4.html#@default448
-Refine,node.1.2.1.html#@default409
-Reflexivity,node.1.2.7.html#@default484
-Remark,node.0.0.2.html#@default43
-Remove LoadPath,node.1.0.4.html#@default340
-Remove Printing If,node.0.1.1.html#@default68
-Remove Printing Let,node.0.1.1.html#@default64
-Rename,node.1.2.2.html#@default417
-Replace ... with,node.1.2.7.html#@default483
-Require,node.1.0.3.html#@default329
-Require Export,node.1.0.3.html#@default330
-Reset,node.1.0.5.html#@default347
-Reset Extraction Inline,node.3.6.1.html#@default636
-Reset Initial,node.1.0.5.html#@default350
-Resource file,node.3.0.2.html#@default576
-Restart,node.1.1.1.html#@default391
-Restore State,node.1.0.5.html#@default349
-Resume,node.1.1.0.html#@default387
-Rewrite,node.1.2.7.html#@default476
-Rewrite ->,node.1.2.7.html#@default477
-Rewrite -> ... in,node.1.2.7.html#@default480
-Rewrite <-,node.1.2.7.html#@default478
-Rewrite <- ... in,node.1.2.7.html#@default481
-Rewrite ... in,node.1.2.7.html#@default479
-Right,node.1.2.5.html#@default460
-Ring,node.1.2.10.html#@default522
-refl_eqT,node.0.2.0.html#@default237
-refl_equal,node.0.2.0.html#@default120
-right,node.0.2.0.html#@default173
-S,node.0.2.0.html#@default140
-Save,node.0.0.2.html#@default49
-Scheme,node.1.2.13.html#@default561
-Script file,node.1.0.2.html#@default324
-Search,node.1.0.1.html#@default313
-Search ... inside ...,node.1.0.1.html#@default317
-Search ... outside ...,node.1.0.1.html#@default320
-SearchAbout,node.1.0.1.html#@default314
-SearchPattern,node.1.0.1.html#@default315
-SearchPattern ... outside ...,node.1.0.1.html#@default321
-SearchRewrite,node.1.0.1.html#@default316
-SearchRewrite ... inside ...,node.1.0.1.html#@default319
-SearchRewrite ... outside ...,node.1.0.1.html#@default322
-Section,node.0.1.3.html#@default72
-Sections,node.0.1.3.html#@default71
-Set,node.0.0.1.html#@default10
-Set Extraction AutoInline,node.3.6.1.html#@default631
-Set Extraction Optimize,#@default629
-Set Hyps_limit,node.1.1.2.html#@default402
-Set Implicit Arguments,node.0.1.7.html#@default87
-Set Printing Coercion,node.3.3.7.html#@default612
-Set Printing Coercions,node.3.3.7.html#@default610
-Set Printing Synth,node.0.1.1.html#@default60
-Set Printing Wildcard,node.0.1.1.html#@default57
-Set Undo,node.1.1.1.html#@default389
-Setoid_replace,node.3.8.html#@default645
-Setoid_rewrite,node.3.8.3.html#@default649
-Show,node.1.1.2.html#@default394
-Show Conjectures,node.1.1.2.html#@default399
-Show Implicits,node.1.1.2.html#@default395
-Show Intro,node.1.1.2.html#@default400
-Show Intros,node.1.1.2.html#@default401
-Show Programs,node.3.5.2.html#@default621
-Show Proof,node.1.1.2.html#@default398
-Show Script,node.1.1.2.html#@default396
-Show Tree,node.1.1.2.html#@default397
-Silent mode,node.1.0.7.html#@default367
-Simpl,node.1.2.4.html#@default450
-Simple Inversion,node.1.2.9.html#@default507
-Simplify_eq,node.1.2.8.html#@default494
-Small inductive type,node.0.3.4.html#@default292
-Snd,node.0.2.0.html#@default156
-Solve,node.1.2.12.html#@default555
-Some,node.0.2.0.html#@default142
-Sorts,node.0.0.1.html#@default8
-Split,node.1.2.5.html#@default457
-SplitAbsolu,node.0.2.1.html#@default251
-SplitRmult,node.0.2.1.html#@default252
-Strong elimination,node.0.3.4.html#@default293
-Structure,node.3.3.8.html#@default615
-Subst,node.1.2.7.html#@default487
-Substitution,node.0.3.0.html#@default262
-Suspend,node.1.1.0.html#@default386
-Symmetry,node.1.2.7.html#@default485
-Syntactic Definition,node.0.1.7.html#@default89
-Syntax,node.1.0.6.html#@default359
-sig,node.0.2.0.html#@default159
-sig2,node.0.2.0.html#@default161
-sigS,node.0.2.0.html#@default165
-sigS2,node.0.2.0.html#@default169
-snd,node.0.2.0.html#@default154
-sort,node.0.0.1.html#@default7
-specif,node.0.0.1.html#@default14
-subgoal,node.1.2.html#@default406
-sum,node.0.2.0.html#@default144
-sum_eqT,node.0.2.0.html#@default238
-sumbool,node.0.2.0.html#@default171
-sumor,node.0.2.0.html#@default175
-sym_eq,node.0.2.0.html#@default122
-sym_not_eq,node.0.2.0.html#@default125
-sym_not_eqT,node.0.2.0.html#@default239
-Tactic Definition,node.1.2.14.html#@default563
-Tacticals,node.1.2.12.html#@default537
-Do,node.1.2.12.html#@default543
-Fail,node.1.2.12.html#@default541
-First,node.1.2.12.html#@default554
-Solve,node.1.2.12.html#@default556
-Idtac,node.1.2.12.html#@default539
-Info,node.1.2.12.html#@default558
-Orelse,node.1.2.12.html#@default545
-Repeat,node.1.2.12.html#@default546
-Try,node.1.2.12.html#@default552
-Tactics,node.1.2.html#@default404
-Tauto,node.1.2.10.html#@default519
-Terms,node.0.0.1.html#@default5
-Test Printing If,node.0.1.1.html#@default69
-Test Printing Let,node.0.1.1.html#@default65
-Test Printing Synth,node.0.1.1.html#@default62
-Test Printing Wildcard,node.0.1.1.html#@default59
-Theorem,node.0.0.2.html#@default41
-Theories,node.0.2.html#@default93
-Time,node.1.0.7.html#@default369
-Transitivity,node.1.2.7.html#@default486
-Transparent,node.1.0.1.html#@default312
-Trivial,node.1.2.10.html#@default516
-True,node.0.2.0.html#@default95
-Try,node.1.2.12.html#@default551
-Type,node.0.0.1.html#@default9
-Type of constructor,node.0.3.4.html#@default289
-Typing rules,node.0.3.1.html#@default265
-Ax,node.0.3.1.html#@default266
-Cases,node.0.3.4.html#@default296
-Const,node.0.3.1.html#@default268
-Conv,node.0.3.2.html#@default282
-Fix,node.0.3.4.html#@default299
-Lam,node.0.3.1.html#@default270
-Let,node.0.3.1.html#@default272
-Prod,node.0.3.1.html#@default269
-Var,node.0.3.1.html#@default267
-tactic macros,node.1.2.14.html#@default562
-trans_eq,node.0.2.0.html#@default123
-trans_eqT,node.0.2.0.html#@default240
-true,node.0.2.0.html#@default136
-tt,node.0.2.0.html#@default134
-Undo,node.1.1.1.html#@default388
-Unfocus,node.1.1.1.html#@default393
-Unfold,node.1.2.4.html#@default451
-Unfold ... in,node.1.2.4.html#@default452
-UnitT,node.0.2.0.html#@default234
-Unset Extraction AutoInline,node.3.6.1.html#@default632
-Unset Extraction Optimize,#@default630
-Unset Hyps_limit,node.1.1.2.html#@default403
-Unset Implicit Arguments,node.1.0.6.html#@default353
-Unset Printing Coercion,node.3.3.7.html#@default613
-Unset Printing Coercions,node.3.3.7.html#@default611
-Unset Printing Synth,node.0.1.1.html#@default61
-Unset Printing Wildcard,node.0.1.1.html#@default58
-Unset Undo,node.1.1.1.html#@default390
-unit,node.0.2.0.html#@default133
-Variable,node.0.0.2.html#@default26
-Variables,node.0.0.2.html#@default27
-value,node.0.2.0.html#@default183
-Well founded induction,node.0.2.0.html#@default214
-Well foundedness,node.0.2.0.html#@default212
-Write State,node.1.0.5.html#@default351
-well_founded,node.0.2.0.html#@default218
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 31edcdd1b7..aeaeb4ec17 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -75,8 +75,8 @@ type pref =
       mutable modifier_for_tactics : Gdk.Tags.modifier list;
       mutable modifiers_valid : Gdk.Tags.modifier list;
 
-      mutable cmd_browse : string * string;
-      mutable cmd_editor : string * string;
+      mutable cmd_browse : string;
+      mutable cmd_editor : string;
 
       mutable text_font : Pango.font_description;
 
@@ -128,10 +128,7 @@ let (current:pref ref) =
 
     
     cmd_browse = Flags.browser_cmd_fmt;
-    cmd_editor = 
-	 if Sys.os_type = "Win32"
-	 then "NOTEPAD ", ""
-	 else "emacs ", "";
+    cmd_editor = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s";
     
 (*    text_font = Pango.Font.from_string "sans 12";*)
     text_font = Pango.Font.from_string "Monospace 10";
@@ -199,8 +196,8 @@ let save_pref () =
       (List.map mod_to_str p.modifier_for_tactics) ++
     add "modifiers_valid" 
       (List.map mod_to_str p.modifiers_valid) ++
-    add "cmd_browse" [fst p.cmd_browse; snd p.cmd_browse] ++
-    add "cmd_editor" [fst p.cmd_editor; snd p.cmd_editor] ++
+    add "cmd_browse" [p.cmd_browse] ++
+    add "cmd_editor" [p.cmd_editor] ++
 
     add "text_font" [Pango.Font.to_string p.text_font] ++
 
@@ -233,6 +230,9 @@ let load_pref () =
     let set_bool k f = set_hd k (fun v -> f (bool_of_string v)) in
     let set_int k f = set_hd k (fun v -> f (int_of_string v)) in
     let set_pair k f = set k (function [v1;v2] -> f v1 v2 | _ -> raise Exit) in
+    let set_command_with_pair_compat k f = 
+      set k (function [v1;v2] -> f (v1^"%s"^v2) | [v] -> f v | _ -> raise Exit)
+    in
     set_hd "cmd_coqc" (fun v -> np.cmd_coqc <- v);
     set_hd "cmd_make" (fun v -> np.cmd_make <- v);
     set_hd "cmd_coqmakefile" (fun v -> np.cmd_coqmakefile <- v);
@@ -257,8 +257,8 @@ let load_pref () =
       (fun v -> np.modifier_for_tactics <- List.map str_to_mod v);
     set "modifiers_valid" 
       (fun v -> np.modifiers_valid <- List.map str_to_mod v);
-    set_pair "cmd_browse" (fun v1 v2 -> np.cmd_browse <- (v1,v2));
-    set_pair "cmd_editor" (fun v1 v2 -> np.cmd_editor <- (v1,v2));
+    set_command_with_pair_compat "cmd_browse" (fun v -> np.cmd_browse <- v);
+    set_command_with_pair_compat "cmd_editor" (fun v -> np.cmd_editor <- v);
     set_hd "text_font" (fun v -> np.text_font <- Pango.Font.from_string v);
     set_hd "doc_url" (fun v -> np.doc_url <- v);
     set_hd "library_url" (fun v -> np.library_url <- v);
@@ -480,20 +480,35 @@ let configure ?(apply=(fun () -> ())) () =
       ~editable:false
       ""
   in
-
   let cmd_editor = 
-    string
-      ~f:(fun s -> !current.cmd_editor <- split_string_format s)
+    let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in
+    combo
       ~help:"(%s for file name)" 
       "External editor"
-      ((fst !current.cmd_editor)^"%s"^(snd !current.cmd_editor))
+      ~f:(fun s -> !current.cmd_editor <- s)
+      ~new_allowed: true
+      (predefined@[if List.mem !current.cmd_editor predefined then ""
+                   else !current.cmd_editor])
+      !current.cmd_editor
   in    
-  let cmd_browse = 
-    string
-      ~f:(fun s -> !current.cmd_browse <- split_string_format s)
+  let cmd_browse =
+    let predefined = [
+      "netscape -remote \"openURL(%s)\"";
+      "mozilla -remote \"openURL(%s)\"";
+      "firefox -remote \"openURL(%s,new-tab)\" || firefox %s &";
+      "firefox -remote \"openURL(%s,new-windows)\" || firefox %s &";
+      "seamonkey -remote \"openURL(%s)\" || seamonkey %s &";
+      "C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s";
+      "open -a Safari %s &"
+    ] in
+    combo 
       ~help:"(%s for url)" 
-      "    Browser"
-      ((fst !current.cmd_browse)^"%s"^(snd !current.cmd_browse))
+      "Browser"
+      ~f:(fun s -> !current.cmd_browse <- s)
+      ~new_allowed: true
+      (predefined@[if List.mem !current.cmd_browse predefined then ""
+                   else !current.cmd_browse])
+      !current.cmd_browse
   in    
   let doc_url = 
     string ~f:(fun s -> !current.doc_url <- s) " Manual URL"  !current.doc_url in
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 9d85b51085..9251730ff2 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -34,8 +34,8 @@ type pref =
       mutable modifier_for_tactics : Gdk.Tags.modifier list;
       mutable modifiers_valid : Gdk.Tags.modifier list;
 
-      mutable cmd_browse : string * string;
-      mutable cmd_editor : string * string;
+      mutable cmd_browse : string;
+      mutable cmd_editor : string;
 
       mutable text_font : Pango.font_description;