diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 8 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 15 |
2 files changed, 17 insertions, 6 deletions
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>> | _ -> |