diff options
| -rw-r--r-- | parsing/g_proofs.ml4 | 2 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 11 | ||||
| -rw-r--r-- | proofs/refiner.ml | 8 | ||||
| -rw-r--r-- | proofs/refiner.mli | 6 | ||||
| -rw-r--r-- | proofs/tactic_debug.ml | 4 | ||||
| -rw-r--r-- | proofs/tactic_debug.mli | 2 | ||||
| -rw-r--r-- | toplevel/cerrors.ml | 3 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
8 files changed, 20 insertions, 18 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 54d68bbea..80dcf23e3 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -35,7 +35,7 @@ GEXTEND Gram ; command: [ [ IDENT "Goal"; c = Constr.lconstr -> VernacGoal c - | IDENT "Proof" -> VernacProof (Tacexpr.TacId "") + | IDENT "Proof" -> VernacProof (Tacexpr.TacId []) | IDENT "Proof"; "with"; ta = tactic -> VernacProof ta | IDENT "Abort" -> VernacAbort None | IDENT "Abort"; IDENT "All" -> VernacAbortAll diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index fcd21098d..e4bc4549b 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -247,6 +247,11 @@ let mlexpr_of_match_rule f = function | Tacexpr.Pat (l,mp,t) -> <:expr< Tacexpr.Pat $mlexpr_of_list mlexpr_of_match_context_hyps l$ $mlexpr_of_match_pattern mp$ $f t$ >> | Tacexpr.All t -> <:expr< Tacexpr.All $f t$ >> +let mlexpr_of_message_token = function + | Tacexpr.MsgString s -> <:expr< Tacexpr.MsgString $str:s$ >> + | Tacexpr.MsgInt n -> <:expr< Tacexpr.MsgInt $mlexpr_of_int n$ >> + | Tacexpr.MsgIdent id -> <:expr< Tacexpr.MsgIdent $mlexpr_of_hyp id$ >> + let rec mlexpr_of_atomic_tactic = function (* Basic tactics *) | Tacexpr.TacIntroPattern pl -> @@ -405,8 +410,10 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function <:expr< Tacexpr.TacRepeat $mlexpr_of_tactic t$ >> | Tacexpr.TacProgress t -> <:expr< Tacexpr.TacProgress $mlexpr_of_tactic t$ >> - | Tacexpr.TacId s -> <:expr< Tacexpr.TacId $str:s$ >> - | Tacexpr.TacFail (n,s) -> <:expr< Tacexpr.TacFail $mlexpr_of_or_var mlexpr_of_int n$ $str:s$ >> + | Tacexpr.TacId l -> + <:expr< Tacexpr.TacId $mlexpr_of_list mlexpr_of_message_token l$ >> + | Tacexpr.TacFail (n,l) -> + <:expr< Tacexpr.TacFail $mlexpr_of_or_var mlexpr_of_int n$ $mlexpr_of_list mlexpr_of_message_token l$ >> (* | Tacexpr.TacInfo t -> TacInfo (loc,f t) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 1bc19c910..dd719e48e 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -335,17 +335,13 @@ let tclIDTAC gls = (goal_goal_list gls, idtac_valid) (* the message printing identity tactic *) let tclIDTAC_MESSAGE s gls = - if s = "" then tclIDTAC gls - else - begin - msgnl (str ("Idtac says : "^s)); tclIDTAC gls - end + msg (hov 0 s); tclIDTAC gls (* General failure tactic *) let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s) (* A special exception for levels for the Fail tactic *) -exception FailError of int * string +exception FailError of int * std_ppcmds (* The Fail tactic *) let tclFAIL lvl s g = raise (FailError (lvl,s)) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index b21485e45..41b312e5d 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -66,7 +66,7 @@ val frontier_mapi : (* [tclIDTAC] is the identity tactic without message printing*) val tclIDTAC : tactic -val tclIDTAC_MESSAGE : string -> tactic +val tclIDTAC_MESSAGE : Pp.std_ppcmds -> tactic (* [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic @@ -123,7 +123,7 @@ val tclTHENLASTn : tactic -> tactic array -> tactic val tclTHENFIRSTn : tactic -> tactic array -> tactic (* A special exception for levels for the Fail tactic *) -exception FailError of int * string +exception FailError of int * Pp.std_ppcmds val tclORELSE : tactic -> tactic -> tactic val tclREPEAT : tactic -> tactic @@ -134,7 +134,7 @@ val tclTRY : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic -val tclFAIL : int -> string -> tactic +val tclFAIL : int -> Pp.std_ppcmds -> tactic val tclDO : int -> tactic -> tactic val tclPROGRESS : tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 5d2cbd57b..43807872d 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -162,10 +162,10 @@ let db_matching_failure debug = (* Prints an evaluation failure message for a rule *) let db_eval_failure debug s = if debug <> DebugOff & !skip = 0 then - let s = if s="" then "no message" else "message \""^s^"\"" in + let s = str "message \"" ++ s ++ str "\"" in msgnl (str "This rule has failed due to \"Fail\" tactic (" ++ - str s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...") + s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...") (* Prints a logic failure message for a rule *) let db_logic_failure debug err = diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index 27536dfa9..a64965605 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -61,7 +61,7 @@ val db_hyp_pattern_failure : val db_matching_failure : debug_info -> unit (* Prints an evaluation failure message for a rule *) -val db_eval_failure : debug_info -> string -> unit +val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit (* An exception handler *) val explain_logic_error: (exn -> Pp.std_ppcmds) ref diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 138df18ed..8342d6800 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -90,8 +90,7 @@ let rec explain_exn_default = function hov 0 (str "Error:" ++ spc () ++ str "No constant of this name:" ++ spc () ++ Libnames.pr_qualid q) | Refiner.FailError (i,s) -> - let s = if s="" then "" else " \""^s^"\"" in - hov 0 (str "Error: Tactic failure" ++ str s ++ + hov 0 (str "Error: Tactic failure" ++ s ++ if i=0 then mt () else str " (level " ++ int i ++ str").") | Stdpp.Exc_located (loc,exc) -> hov 0 ((if loc = dummy_loc then (mt ()) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f7ba9e8117..c08b52727 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -563,7 +563,7 @@ let vernac_solve_existential = instantiate_nth_evar_com let vernac_set_end_tac tac = if not (refining ()) then error "Unknown command of the non proof-editing mode"; - if tac <> (Tacexpr.TacId "") then set_end_tac (Tacinterp.interp tac) + if tac <> (Tacexpr.TacId []) then set_end_tac (Tacinterp.interp tac) (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) |