diff options
| author | Pierre-Marie Pédrot | 2016-06-03 17:10:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-03 17:11:07 +0200 |
| commit | 89a1ea67a72500eeae1d003dd346f01ded514f7b (patch) | |
| tree | 8134c12bef64decc00490519f2f04e06932355e0 /ltac/extraargs.ml4 | |
| parent | 9d60ddc84e95a030913fc4b3db705f3ec894fdb2 (diff) | |
| parent | 3206bf597d63066d9d9f8adfd0fe76e3c1c97e4d (diff) | |
Remove a few tactics from the Tacexpr AST.
Note that this breaks a few badly written scripts using intro in strict
mode without providing an existing identifier.
Diffstat (limited to 'ltac/extraargs.ml4')
| -rw-r--r-- | ltac/extraargs.ml4 | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index 0bddcc9fdd..e6d0a9c69c 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -15,6 +15,7 @@ open Constrarg open Pcoq.Prim open Pcoq.Constr open Names +open Tacmach open Tacexpr open Taccoerce open Tacinterp @@ -175,6 +176,16 @@ ARGUMENT EXTEND lglob [ lconstr(c) ] -> [ c ] END +let interp_casted_constr ist gl c = + interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c + +ARGUMENT EXTEND casted_constr + TYPED AS constr + PRINTED BY pr_gen + INTERPRETED BY interp_casted_constr + [ constr(c) ] -> [ c ] +END + type 'id gen_place= ('id * hyp_location_flag,unit) location type loc_place = Id.t Loc.located gen_place @@ -225,6 +236,14 @@ ARGUMENT EXTEND hloc END +let pr_rename _ _ _ (n, m) = Nameops.pr_id n ++ str " into " ++ Nameops.pr_id m + +ARGUMENT EXTEND rename + TYPED AS ident * ident + PRINTED BY pr_rename +| [ ident(n) "into" ident(m) ] -> [ (n, m) ] +END + (* Julien: Mise en commun des differentes version de replace with in by *) let pr_by_arg_tac _prc _prlc prtac opt_c = |