removes a lot comments that may be useful for later code maintenance, but

should not be kept in the sources because they only contain obsolete code


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

1 files changed, 0 insertions, 303 deletions

diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index c86d12ad2..f3d3988e2 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -54,9 +54,6 @@ let if_pcoq f a =
 
 let text_proof_flag = ref "en";;
 
-(* 
-let current_proof_name = ref "";;
-*)
 let current_proof_name () = 
   try 
     string_of_id (get_current_proof_name ())
@@ -606,305 +603,12 @@ let pcoq_hook = {
   show_goal = pcoq_show_goal
 }
 
-(*
-let command_changes = [
-  ("TEXT_MODE",
-   (function
-     |  [Coqast.VARG_AST (Str(_,x))] ->
-	 (fun () -> set_text_mode x)));
-
-  ("StartProof", 
-   (function
-     | (Coqast.VARG_STRING kind) ::
-       ((Coqast.VARG_IDENTIFIER s) ::
-	((Coqast.VARG_CONSTR c) :: [])) ->
-	  let stre =
-	    match kind with
-	    | "THEOREM" -> NeverDischarge
-	    | "LEMMA" -> NeverDischarge
-	    | "FACT" -> make_strength_1 ()
-	    | "REMARK" -> make_strength_0 ()
-	    | "DEFINITION" -> NeverDischarge
-	    | "LET" -> make_strength_2 ()
-	    | "LETTOP" -> NotDeclare
-	    | "LOCAL" -> make_strength_0 ()
-	    | _ -> errorlabstrm "StartProof" (make_error_stream "StartProof") in
-	  fun () ->
-	    begin
-	      if kind = "LETTOP" && not(refining ()) then
-		errorlabstrm "StartProof"
-		  (str
-		     "Let declarations can only be used in proof editing mode"
-		  );
-		let str = (string_of_id s) in
-		start_proof_com (Some s) stre c;
-		start_proof_hook str;
-	    end
-     | _ -> errorlabstrm "StartProof" (make_error_stream "StartProof")));
-
-  ("GOAL", 
-   (function
-     | (Coqast.VARG_CONSTR c) :: [] ->
-	 (fun () ->
-	    if not (refining ()) then
-	      begin
-		start_proof_com None NeverDischarge c;
-                start_proof_hook "Unnamed_thm"
-	      end)
-     | [] ->
-	 (function () -> output_results_nl(ctf_EmptyGoalMessage ""))
-     | _ -> errorlabstrm "Goal" (make_error_stream "Goal")));
-  
-  ("SOLVE",
-   (function
-     | [Coqast.VARG_NUMBER n; Coqast.VARG_TACTIC tcom] ->
-       (fun () -> 
-         if not (refining ()) then
-           error "Unknown command of the non proof-editing mode";
-         solve_nth n (Tacinterp.hide_interp tcom);
-(* pcoq *)
-         solve_hook n
-(**)
-     | _ -> errorlabstrm "SOLVE" (make_error_stream "SOLVE")));
-
-(* SIMULE SOLVE SANS EFFET *)
-  ("GOAL_CMD", 
-   (function
-     | (Coqast.VARG_NUMBER n) ::
-       ((Coqast.VARG_TACTIC tac) :: []) ->
-	 (function () -> 
-	    let path = History.get_nth_open_path !current_proof_name n in
-              solve_nth n (Tacinterp.hide_interp tac);
-              traverse_to path;
-              Pfedit.mutate weak_undo_pftreestate;
-	      traverse_to [])
-     | _ -> errorlabstrm "GOAL_CMD" (make_error_stream "GOAL_CMD")));
-
-(* Revient à l'état avant l'application de la n-ième tactique *)
-  ("KILL_NODE", 
-   (function
-     | (Coqast.VARG_NUMBER n) :: [] ->
-	 (function () -> 
-	   let ngoals = kill_proof_node n in
-	   output_results_nl
-             (ctf_KilledMessage !global_request_id ngoals))
-     | _ -> errorlabstrm "KILL_NODE" (make_error_stream "KILL_NODE")));
-(* Annule toutes les commandes qui s'appliquent sur les sous-buts du
-   but auquel a été appliquée la n-ième tactique *)
-  ("KILL_SUB_PROOF",
-   (function
-     | [Coqast.VARG_NUMBER n] ->
-	 (function () -> logical_kill n)
-     | _ -> errorlabstrm "KILL_SUB_PROOF" (make_error_stream "KILL_SUB_PROOF")));
-
-  ("RESUME",
-   (function [Coqast.VARG_IDENTIFIER id] ->
-     (fun () -> 
-       let str = (string_of_id id) in
-	 resume_proof id;
-(* Pcoq *)
-	 current_proof_name := str)
-(**)
-      | _ -> errorlabstrm "RESUME" (make_error_stream "RESUME")));
-
-(* NoOp... *)
-  ("BeginSilent", 
-   (function
-     | [] ->
-	 (function
-	     () ->
-	       errorlabstrm "Begin Silent" 
-		 (str "not available in Centaur mode"))
-     | _ -> errorlabstrm "BeginSilent" (make_error_stream "BeginSilent")));
-  
-  ("EndSilent", 
-   (function
-     | [] ->
-	 (function
-	     () ->
-	       errorlabstrm "End Silent"
-		 (str "not available in Centaur mode"))
-     | _ -> errorlabstrm "EndSilent" (make_error_stream "EndSilent")));
-  
-  ("ABORT", 
-   (function
-     | (Coqast.VARG_IDENTIFIER id) :: [] ->
-	 (function
-	     () ->
-	       delete_proof id;
-(* Pcoq *)
-	       current_proof_name := "";
-	       output_results_nl
-		 (ctf_AbortedMessage !global_request_id (string_of_id id)))
-(**)
-     | [] ->
-	 (function
-	     () -> delete_current_proof ();
-(* Pcoq *)
-	     current_proof_name := "";
-	       output_results_nl
-		 (ctf_AbortedMessage !global_request_id ""))
-(**)
-     | _ -> errorlabstrm "ABORT" (make_error_stream "ABORT")));
-  ("SEARCH",
-   function
-       (Coqast.VARG_QUALID qid)::l ->
-         (fun () -> 
-           ctv_SEARCH_LIST:=[];
-	    let global_ref = Nametab.global dummy_loc qid in
-           filtered_search
-             (filter_by_module_from_varg_list l)
-	     add_search (Nametab.locate qid);
-	   search_output_results())
-     |	_ -> failwith "bad form of arguments");
-
-  ("SearchRewrite",
-   function
-       (Coqast.VARG_CONSTR c)::l ->
-	 (fun () -> 
-            ctv_SEARCH_LIST:=[];
-	    let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
-              raw_search_rewrite
-             	(filter_by_module_from_varg_list l)
-             	add_search pat;
-              search_output_results())
-     |	_ -> failwith "bad form of arguments");
-
-  ("SearchPattern",
-   function
-       (Coqast.VARG_CONSTR c)::l ->
-	 (fun () ->
-	    ctv_SEARCH_LIST := [];
-	    let _,pat = interp_constrpattern Evd.empty (Global.env()) c in
-	      raw_pattern_search
-             	(filter_by_module_from_varg_list l)
-             	add_search pat;
-	      search_output_results())
-     |	_ -> failwith "bad form of arguments");
-  
-  ("PrintId",
-   (function
-      | [Coqast.VARG_QUALID qid] ->
-	 (function () -> 
-	   let results = xlate_vernac_list (Ctast.ast_to_ct (name_to_ast qid)) in
-	   output_results 
-	     (fnl () ++ str "message" ++ fnl () ++ str "PRINT_VALUE" ++ fnl ())
-	     (Some (P_cl results)))
-     | _ -> errorlabstrm "PrintId" (make_error_stream "PrintId")));
-  
-  ("Check", 
-   (function
-     | (Coqast.VARG_STRING kind) :: ((Coqast.VARG_CONSTR c) :: g) ->
-	 let evmap, env =
-	   Vernacentries.get_current_context_of_args g in
-	 let f =
-	   match kind with
-	   | "CHECK" -> print_check
-	   | "PRINTTYPE" ->
-	       errorlabstrm "PrintType" (str "Not yet supported in CtCoq")
-	   | _ -> errorlabstrm "CHECK" (make_error_stream "CHECK") in
-	 (function () -> 
-	   let a,b = f (c, judgment_of_rawconstr evmap env c) in
-	   output_results a b)
-     | _ -> errorlabstrm "CHECK" (make_error_stream "CHECK")));
-  
-  ("Eval",
-   (function
-     | Coqast.VARG_TACTIC_ARG(Redexp redexp):: Coqast.VARG_CONSTR c :: g ->
-	 let evmap, env = Vernacentries.get_current_context_of_args g in
-	 let redfun =
-	   ct_print_eval (Ctast.ast_to_ct c) (Tacred.reduction_of_redexp redexp env evmap) env in
-	 fun () -> 
-	   let strm, vtp = redfun evmap (judgment_of_rawconstr evmap env c) in
-	   output_results strm vtp
-     | _ -> errorlabstrm "Eval" (make_error_stream "Eval")));
-  
-  ("Centaur_Reset", 
-   (function
-     | (Coqast.VARG_IDENTIFIER c) :: [] ->
-	 if refining () then 
-	   output_results (ctf_AbortedAllMessage ()) None;
-	   current_proof_name := "";
-	 (match string_of_id c with
-	 | "CtCoqInitialState" ->
-	     (function
-		 () ->
-		   current_proof_name := "";
-		   Vernacentries.abort_refine Lib.reset_initial ();
-		   output_results (ctf_ResetInitialMessage ()) None)
-	 | _ ->
-	     (function
-		 () ->
-		   current_proof_name := "";
-		   Vernacentries.abort_refine Lib.reset_name c;
-		   output_results
-		     (ctf_ResetIdentMessage
-			!global_request_id (string_of_id c)) None))
-     | _ -> errorlabstrm "Centaur_Reset" (make_error_stream "Centaur_Reset")));
-  ("Show_dad_rules",
-   (function
-     | [] ->
-	 (fun () -> 
-	   let results = dad_rule_names() in
-	   output_results
-	     (ctf_header "dad_rule_names" !global_request_id)
-	     (Some (P_ids
-		      (CT_id_list
-			 (List.map (fun s -> CT_ident s) results)))))
-     | _ ->
-	 errorlabstrm
-	   "Show_dad_rules" (make_error_stream "Show_dad_rules")));
-  ("INSPECT",
-   (function
-     | [Coqast.VARG_NUMBER n] ->
-         (function () -> inspect n)
-     | _ -> errorlabstrm "INSPECT" (make_error_stream "INSPECT")))
-
-];;
-*)
-(*
-let non_debug_changes = [
-  ("SHOW", 
-   (function
-     | [Coqast.VARG_NUMBER n] -> (function () -> show_nth n)
-     | _ -> errorlabstrm "SHOW" (make_error_stream "SHOW")))];;
-*)
-
-(* Moved to Vernacentries...
-let command_creations = [
-  ("Comments",
-   function l -> (fun () -> message ("Comments ok\n")));
-(* Dead code
-  ("CommentsBold",
-   function l -> (fun () -> message ("CommentsBold ok\n")));
-  ("Title",
-   function l -> (fun () -> message ("Title ok\n")));
-  ("Author",
-   function l -> (fun () -> message ("Author ok\n")));
-  ("Note",
-   function l -> (fun () -> message ("Note ok\n")));
-  ("NL",
-   function l -> (fun () -> message ("Newline ok\n")))
-*)
-];;
-*)
 
 TACTIC EXTEND Pbp
 | [ "Pbp" ident_opt(idopt) natural_list(nl) ] -> 
     [ if_pcoq pbp_tac_pcoq idopt nl ]
 END
 
-(* <\cpa> 
-TACTIC EXTEND Blast
-| [ "Blast" ne_natural_list(nl) ] ->
-    [ if_pcoq blast_tac_pcoq nl ]
-END
-TACTIC EXTEND Dad
-| [ "Dad" natural_list(nl1) "to" natural_list(nl2) ] ->
-    [ if_pcoq dad_tac_pcoq nl1 nl2 ]
-END
- </cpa> *)
-
 TACTIC EXTEND CtDebugTac
 | [ "DebugTac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
 END
@@ -921,13 +625,6 @@ let start_pcoq_mode debug =
     start_dad();
 </cpa> *)
     declare_in_coq();
-(*
-    add_tactic "PcoqPbp" pbp_tac_pcoq;
-    add_tactic "PcoqBlast" blast_tac_pcoq;
-    add_tactic "Dad" dad_tac_pcoq;
-    add_tactic "CtDebugTac" debug_tac2_pcoq;
-    add_tactic "CtDebugTac2" debug_tac2_pcoq;
-*)
 (* The following ones are added to enable rich comments in pcoq *)
 (* TODO ...
     add_tactic "Image" (fun _ -> tclIDTAC);