diff options
| author | herbelin | 2003-03-31 21:18:53 +0000 |
|---|---|---|
| committer | herbelin | 2003-03-31 21:18:53 +0000 |
| commit | 00608fac2d8e217232d5f2ddd28a43971bf259b7 (patch) | |
| tree | 0bd65009594d83c85a6e3f4f5bf8a0e77e0b4fc6 /contrib | |
| parent | ca29570a25be8f9b8757399f5f0b72b4a9bd5e43 (diff) | |
Ajout d'un message à FailTac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/funind/tacinv.ml4 | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 4 | ||||
| -rwxr-xr-x | contrib/linear/ccidpc.ml4 | 10 |
3 files changed, 9 insertions, 7 deletions
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 index 6bc310460d..3137a38ad1 100644 --- a/contrib/funind/tacinv.ml4 +++ b/contrib/funind/tacinv.ml4 @@ -528,7 +528,7 @@ let rec iterintro i = let hypname = (string_of_id (destVar hyp)) in let sub = try String.sub hypname 0 4 with _ -> "" (* different than "_eq_" *) in - if sub="_eq_" then rewriteLR hyp else tclFAIL 0) + if sub="_eq_" then rewriteLR hyp else tclFAIL 0 "Cannot rewrite") )) gl) diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 3941d10c6f..8191a0978f 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -758,7 +758,8 @@ and xlate_tactic = (xlate_local_rec_tac f1, List.map xlate_local_rec_tac l) in CT_rec_tactic_in(tl, xlate_tactic t) | TacAtom (_, t) -> xlate_tac t - | TacFail n -> CT_fail (CT_int n) + | TacFail (n,"") -> CT_fail (CT_int n) + | TacFail (n,s) -> xlate_error "TODO: Fail n message" | TacId -> CT_idtac | TacInfo t -> CT_info(xlate_tactic t) | TacArg a -> xlate_call_or_tacarg a @@ -1656,6 +1657,7 @@ let xlate_vernac = match opt_positions with None -> CT_int_list[] | Some l -> CT_int_list(List.map (fun x -> CT_int x) l)) + | VernacReserve _ -> xlate_error "TODO: Default Variable Type" | VernacLocate(LocateTerm id) -> CT_locate(reference_to_ct_ID id) | VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id) | VernacLocate(LocateFile s) -> CT_locate_file(CT_string s) diff --git a/contrib/linear/ccidpc.ml4 b/contrib/linear/ccidpc.ml4 index 09b81f349c..a9b3e50ee7 100755 --- a/contrib/linear/ccidpc.ml4 +++ b/contrib/linear/ccidpc.ml4 @@ -206,33 +206,33 @@ let rec alpha_term bl1 bl2 p_0 p_1 = let forAllI id gls=if is_forall_term (pf_concl gls) then - intro_using id gls else tclFAIL 0 gls + intro_using id gls else tclFAIL 0 "goal is not universally quantified" gls let forAllE id t gls = let rgl=pf_whd_betadeltaiota gls (pf_type_of gls (mkVar id)) in if is_forall_term rgl then tclTHEN (generalize [mkApp (mkVar id,[|t|])]) intro gls - else tclFAIL 0 gls + else tclFAIL 0 "hypothesis is not universally quantified" gls let existE id id2 gls = let (_,_,t)=lookup_named id (pf_hyps gls) in if is_exist_term t then ((tclTHEN (simplest_elim (mkVar id)) (tclTHEN (intro_using id2) (dImp None)))) gls - else tclFAIL 0 gls + else tclFAIL 0 "hypothesis is not existentially quantified" gls let negE id gls = let (_,_,t)=lookup_named id (pf_hyps gls) in if is_not_term t then (simplest_elim (mkVar id)) gls - else tclFAIL 0 gls + else tclFAIL 0 "hypothesis is not negated" gls (*t exist_intro_head = put_pat mmk "ex_intro"*) let existI t gls = if is_exist_term (pf_concl gls) then split (Rawterm.ImplicitBindings [t]) gls - else tclFAIL 0 gls + else tclFAIL 0 "goal is not existentially quantified" gls (* let (wc,kONT) = Evar_refiner.startWalk gls in |