diff options
author | 2006-01-21 11:09:18 +0000 | |
---|---|---|
committer | 2006-01-21 11:09:18 +0000 | |
commit | 1766059a85a44893839ee52e0840f26638da02bf (patch) | |
tree | 24a771a1288b6104683abd7efd3a385c035e8203 | |
parent | d7fcf7e0ef2fcee500a1436b8b9d5c0b8a5c8530 (diff) |
Messages de idtac et fail peuvent maintenant ĂȘtre des listes de string, int et variables ltac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7909 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/cc/cctac.ml | 4 | ||||
-rw-r--r-- | contrib/first-order/g_ground.ml4 | 2 | ||||
-rw-r--r-- | contrib/first-order/ground.ml | 2 | ||||
-rw-r--r-- | contrib/first-order/instances.ml | 6 | ||||
-rw-r--r-- | contrib/first-order/rules.ml | 6 | ||||
-rw-r--r-- | contrib/funind/tacinv.ml4 | 2 | ||||
-rw-r--r-- | contrib/recdef/recdef.ml4 | 2 | ||||
-rw-r--r-- | tactics/auto.ml | 2 | ||||
-rw-r--r-- | tactics/extratactics.ml4 | 2 | ||||
-rw-r--r-- | tactics/tacticals.ml | 4 | ||||
-rw-r--r-- | tactics/tacticals.mli | 5 |
11 files changed, 19 insertions, 18 deletions
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml index a3e1902c0..e6ce0ad66 100644 --- a/contrib/cc/cctac.ml +++ b/contrib/cc/cctac.ml @@ -287,7 +287,7 @@ let cc_tactic additionnal_terms gls= let _ = debug Pp.msgnl (Pp.str "Computation completed.") in let uf=forest state in match sol with - None -> tclFAIL 0 "congruence failed" gls + None -> tclFAIL 0 (str "congruence failed") gls | Some reason -> debug Pp.msgnl (Pp.str "Goal solved, generating proof ..."); match reason with @@ -318,7 +318,7 @@ let cc_tactic additionnal_terms gls= end); Pp.msgnl (Pp.str " replacing metavariables by arbitrary terms."); - tclFAIL 0 "Incomplete" gls + tclFAIL 0 (str "Incomplete") gls | Contradiction dis -> let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in let ta=term uf dis.lhs and tb=term uf dis.rhs in diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4 index 0db32a555..e6f7b03cb 100644 --- a/contrib/first-order/g_ground.ml4 +++ b/contrib/first-order/g_ground.ml4 @@ -41,7 +41,7 @@ let _= let default_solver=(Tacinterp.interp <:tactic<auto with *>>) -let fail_solver=tclFAIL 0 "GTauto failed" +let fail_solver=tclFAIL 0 (Pp.str "GTauto failed") type external_env= Ids of global_reference list diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml index 00a2260c6..9f9a7e68d 100644 --- a/contrib/first-order/ground.ml +++ b/contrib/first-order/ground.ml @@ -78,7 +78,7 @@ let ground_tac solver startseq gl= | Rforall-> let backtrack1= if !qflag then - tclFAIL 0 "reversible in 1st order mode" + tclFAIL 0 (Pp.str "reversible in 1st order mode") else backtrack in forall_tac backtrack continue (re_add seq1) diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml index 0b371966b..eac842b86 100644 --- a/contrib/first-order/instances.ml +++ b/contrib/first-order/instances.ml @@ -138,7 +138,7 @@ let left_instance_tac (inst,id) continue seq= match inst with Phantom dom-> if lookup (id,None) seq then - tclFAIL 0 "already done" + tclFAIL 0 (Pp.str "already done") else tclTHENS (cut dom) [tclTHENLIST @@ -152,7 +152,7 @@ let left_instance_tac (inst,id) continue seq= tclTRY assumption] | Real((m,t) as c,_)-> if lookup (id,Some c) seq then - tclFAIL 0 "already done" + tclFAIL 0 (Pp.str "already done") else let special_generalize= if m>0 then @@ -186,7 +186,7 @@ let right_instance_tac inst continue seq= (tclTHEN (split (Rawterm.ImplicitBindings [t])) (tclSOLVE [wrap 0 true continue (deepen seq)])) | Real ((m,t),_) -> - tclFAIL 0 "not implemented ... yet" + tclFAIL 0 (Pp.str "not implemented ... yet") let instance_tac inst= if (snd inst)==dummy_id then diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml index 727a03000..bc4699ea1 100644 --- a/contrib/first-order/rules.ml +++ b/contrib/first-order/rules.ml @@ -58,7 +58,7 @@ let clear_global=function let axiom_tac t seq= try exact_no_check (constr_of_global (find_left t seq)) - with Not_found->tclFAIL 0 "No axiom link" + with Not_found->tclFAIL 0 (Pp.str "No axiom link") let ll_atom_tac a backtrack id continue seq= tclIFTHENELSE @@ -68,7 +68,7 @@ let ll_atom_tac a backtrack id continue seq= [|constr_of_global (find_left a seq)|])]; clear_global id; intro] - with Not_found->tclFAIL 0 "No link") + with Not_found->tclFAIL 0 (Pp.str "No link")) (wrap 1 false continue seq) backtrack (* right connectives rules *) @@ -168,7 +168,7 @@ let forall_tac backtrack continue seq= (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq))) backtrack)) (if !qflag then - tclFAIL 0 "reversible in 1st order mode" + tclFAIL 0 (Pp.str "reversible in 1st order mode") else backtrack) diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 index 27c0658d2..bf918ba56 100644 --- a/contrib/funind/tacinv.ml4 +++ b/contrib/funind/tacinv.ml4 @@ -597,7 +597,7 @@ let rec iterintro i = let sub = try String.sub hypname 0 (String.length heq_prefix) with _ -> "" (* different than [heq_prefix] *) in - if sub=heq_prefix then rewriteLR hyp else tclFAIL 0 "Cannot rewrite") + if sub=heq_prefix then rewriteLR hyp else tclFAIL 0 (str "Cannot rewrite")) )) gl) diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 1671c405a..2e62aa407 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -247,7 +247,7 @@ let list_rewrite (rev:bool) (eqs: constr list) = tclREPEAT (List.fold_right (fun eq i -> tclORELSE (rewriteLR eq) i) - (if rev then (List.rev eqs) else eqs) (tclFAIL 0 ""));; + (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));; let base_leaf (func:global_reference) eqs expr = (* let _ = msgnl (str "entering base_leaf") in *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 4f8df90b5..cc6dc33e6 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -862,7 +862,7 @@ let compileAutoArg contac = function then tclTHENSEQ [simplest_elim (mkVar id); clear [id]; contac] else - tclFAIL 0 ((string_of_id id)^"is not a conjunction")) + tclFAIL 0 (pr_id id ++ str" is not a conjunction")) ctx) g) | UsingTDB -> (tclTHEN diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index fbd881789..7aae9f522 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -138,7 +138,7 @@ let add_rewrite_hint name ort t lcsr = VERNAC COMMAND EXTEND HintRewrite [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident(b) ] -> - [ add_rewrite_hint b o (Tacexpr.TacId "") l ] + [ add_rewrite_hint b o (Tacexpr.TacId []) l ] | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ":" preident(b) ] -> [ add_rewrite_hint b o t l ] diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 517d774d4..3b5349a4b 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -91,7 +91,7 @@ let tclLAST_HYP = tclNTH_HYP 1 let tclTRY_sign (tac : constr->tactic) sign gl = let rec arec = function - | [] -> tclFAIL 0 "no applicable hypothesis" + | [] -> tclFAIL 0 (str "no applicable hypothesis") | [s] -> tac (mkVar s) (*added in order to get useful error messages *) | (s::sl) -> tclORELSE (tac (mkVar s)) (arec sl) in @@ -133,7 +133,7 @@ let simple_clause_list_of cl gls = (* OR-branch *) let tryClauses tac cl gls = let rec firstrec = function - | [] -> tclFAIL 0 "no applicable hypothesis" + | [] -> tclFAIL 0 (str "no applicable hypothesis") | [cls] -> tac cls (* added in order to get a useful error message *) | cls::tl -> (tclORELSE (tac cls) (firstrec tl)) in diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 699c0d780..4b0e39e78 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -9,6 +9,7 @@ (*i $Id$ i*) (*i*) +open Pp open Names open Term open Sign @@ -24,7 +25,7 @@ open Tacexpr (* Tacticals i.e. functions from tactics to tactics. *) val tclIDTAC : tactic -val tclIDTAC_MESSAGE : string -> tactic +val tclIDTAC_MESSAGE : std_ppcmds -> tactic val tclORELSE : tactic -> tactic -> tactic val tclTHEN : tactic -> tactic -> tactic val tclTHENSEQ : tactic list -> tactic @@ -46,7 +47,7 @@ val tclTRY : tactic -> tactic val tclINFO : tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic -val tclFAIL : int -> string -> tactic +val tclFAIL : int -> std_ppcmds -> tactic val tclDO : int -> tactic -> tactic val tclPROGRESS : tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic |