diff options
| author | herbelin | 2011-10-25 21:02:53 +0000 |
|---|---|---|
| committer | herbelin | 2011-10-25 21:02:53 +0000 |
| commit | b020c6c4d9f1fdd5f5e17f0b08151a18f021f8d3 (patch) | |
| tree | 14e9e94fe5bddb75916485c1dce76baad6f32fef /tactics | |
| parent | b91f721df622b40e1f4ca610dd4a5697d27ec56a (diff) | |
Applying Tom Prince's patch to support parametric "constructor n" in
tactic notations and ltac definitions (see bug report #2496).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14606 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hiddentac.ml | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 4 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 4 |
3 files changed, 7 insertions, 5 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index c5a2f87b6e..fafc681ae2 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -111,9 +111,9 @@ let h_any_constructor t = abstract_tactic (TacAnyConstructor t) (any_constructor t) *) let h_constructor ev n l = - abstract_tactic (TacConstructor(ev,AI n,l))(constructor_tac ev None n l) + abstract_tactic (TacConstructor(ev,ArgArg n,l))(constructor_tac ev None n l) let h_one_constructor n = - abstract_tactic (TacConstructor(false,AI n,NoBindings)) (one_constructor n NoBindings) + abstract_tactic (TacConstructor(false,ArgArg n,NoBindings)) (one_constructor n NoBindings) let h_simplest_left = h_left false NoBindings let h_simplest_right = h_right false NoBindings diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d0fcad21a9..a88c5f79b7 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -762,7 +762,7 @@ let rec intern_atomic lf ist x = | TacRight (ev,bl) -> TacRight (ev,intern_bindings ist bl) | TacSplit (ev,b,bll) -> TacSplit (ev,b,List.map (intern_bindings ist) bll) | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_tactic ist) t) - | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,intern_bindings ist bl) + | TacConstructor (ev,n,bl) -> TacConstructor (ev,intern_or_var ist n,intern_bindings ist bl) (* Conversion *) | TacReduce (r,cl) -> @@ -2323,7 +2323,7 @@ and interp_atomic ist gl tac = (Tactics.any_constructor ev (Option.map (interp_tactic ist) t)) | TacConstructor (ev,n,bl) -> let sigma, bl = interp_bindings ist env sigma bl in - tclWITHHOLES ev (h_constructor ev (skip_metaid n)) sigma bl + tclWITHHOLES ev (h_constructor ev (interp_int_or_var ist n)) sigma bl (* Conversion *) | TacReduce (r,cl) -> diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index a9d4bd8899..46f8c9bb4b 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -152,10 +152,12 @@ let flatten_contravariant_disj ist = let hyp = valueIn (VConstr ([],hyp)) in iter_tac (list_map_i (fun i arg -> let typ = valueIn (VConstr ([],mkArrow arg c)) in + let i = Tacexpr.Integer i in <:tactic< let typ := $typ in let hyp := $hyp in - assert typ by (intro; apply hyp; constructor $i; assumption) + let i := $i in + assert typ by (intro; apply hyp; constructor i; assumption) >>) 1 args) <:tactic< let hyp := $hyp in clear hyp >> else <:tactic<fail>> |