diff options
| author | herbelin | 2009-09-26 13:07:52 +0000 |
|---|---|---|
| committer | herbelin | 2009-09-26 13:07:52 +0000 |
| commit | 8c6fb6f52db5bfda6cdfeb4f581da1332fb4a20b (patch) | |
| tree | b1d59369165c2b22368662a13d1eb79971c247b1 /tactics | |
| parent | 9abfed86acb129d836423e73d05f1a53766c56a7 (diff) | |
Fixed a hole in glob_tactic that allowed some Ltac code to refer to
statically unbound variables (revealed by an assert failure in
Tacinterp.subst_rawconstr_and_expr). In particular, tauto's use of
name "id" was bypassing the globalization phase (apparently in an safe
way though).
Added a new kind of anomaly usable in case an anomaly results of an
unexpected exception.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12354 85f007b7-540e-0410-9357-904b9bb8a0f7
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>> | _ -> |