diff options
| -rw-r--r-- | lib/util.ml | 2 | ||||
| -rw-r--r-- | lib/util.mli | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 8 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 15 | ||||
| -rw-r--r-- | toplevel/cerrors.ml | 3 |
5 files changed, 24 insertions, 6 deletions
diff --git a/lib/util.ml b/lib/util.ml index ddf44eec37..2815af0145 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -20,6 +20,8 @@ exception UserError of string * std_ppcmds (* User errors *) let error string = raise (UserError(string, str string)) let errorlabstrm l pps = raise (UserError(l,pps)) +exception AnomalyOnError of string * exn + let todo s = prerr_string ("TODO: "^s^"\n") exception Timeout diff --git a/lib/util.mli b/lib/util.mli index 4579982bcf..4e2bb6d339 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -26,6 +26,8 @@ exception UserError of string * std_ppcmds val error : string -> 'a val errorlabstrm : string -> std_ppcmds -> 'a +exception AnomalyOnError of string * exn + (* [todo] is for running of an incomplete code its implementation is "do nothing" (or print a message), but this function should not be used in a released code *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 427a6eaa67..ecf4ba9a53 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2899,7 +2899,8 @@ let add_tacdef isrec tacl = (***************************************************************************) (* Other entry points *) -let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x +let glob_tactic x = + Flags.with_option strict_check (intern_tactic (make_empty_glob_sign ())) x let glob_tactic_env l env x = Flags.with_option strict_check @@ -2916,7 +2917,10 @@ let interp_redexp env sigma r = (* Embed tactics in raw or glob tactic expr *) let globTacticIn t = TacArg (TacDynamic (dummy_loc,tactic_in t)) -let tacticIn t = globTacticIn (fun ist -> glob_tactic (t ist)) +let tacticIn t = + globTacticIn (fun ist -> + try glob_tactic (t ist) + with e -> raise (AnomalyOnError ("Incorrect tactic expression", e))) let tacticOut = function | TacArg (TacDynamic (_,d)) -> diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index ebfb9446f3..6fea983772 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -20,6 +20,7 @@ open Tacticals open Tacinterp open Tactics open Util +open Genarg let assoc_var s ist = match List.assoc (Names.id_of_string s) ist.lfun with @@ -108,18 +109,21 @@ let is_conj ist = let flatten_contravariant_conj ist = let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in + let hyp = assoc_var "id" ist in match match_with_conjunction ~strict:strict_in_contravariant_hyp typ with | Some (_,args) -> let i = List.length args in if not binary_mode || i = 2 then let newtyp = valueIn (VConstr (List.fold_right mkArrow args c)) in + let hyp = valueIn (VConstr hyp) in let intros = iter_tac (List.map (fun _ -> <:tactic< intro >>) args) <:tactic< idtac >> in <:tactic< let newtyp := $newtyp in - assert newtyp by ($intros; apply id; split; assumption); - clear id + let hyp := $hyp in + assert newtyp by ($intros; apply hyp; split; assumption); + clear hyp >> else <:tactic<fail>> @@ -140,16 +144,19 @@ let is_disj ist = let flatten_contravariant_disj ist = let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in + let hyp = assoc_var "id" ist in match match_with_disjunction ~strict:strict_in_contravariant_hyp typ with | Some (_,args) -> let i = List.length args in if not binary_mode || i = 2 then + let hyp = valueIn (VConstr hyp) in iter_tac (list_map_i (fun i arg -> let typ = valueIn (VConstr (mkArrow arg c)) in <:tactic< let typ := $typ in - assert typ by (intro; apply id; constructor $i; assumption) - >>) 1 args) <:tactic< clear id >> + let hyp := $hyp in + assert typ by (intro; apply hyp; constructor $i; assumption) + >>) 1 args) <:tactic< let hyp := $hyp in clear hyp >> else <:tactic<fail>> | _ -> diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index dfedc178fb..08c0bac1c8 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -49,6 +49,9 @@ let rec explain_exn_default_aux anomaly_string report_fn = function hov 0 (str "Timeout!") | Anomaly (s,pps) -> hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ()) + | AnomalyOnError (s,exc) -> + hov 0 (anomaly_string () ++ str s ++ str ". Received exception is:" ++ + fnl() ++ explain_exn_default_aux anomaly_string report_fn exc) | Match_failure(filename,pos1,pos2) -> hov 0 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++ if Sys.ocaml_version = "3.06" then |