diff options
| author |  clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-17 16:10:42 +0000 |
|---|---|---|
| committer | clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-17 16:10:42 +0000 |
| commit | 4d2d218a6296fad88225ceea66f08355ec6d9a5c (patch) | |
| tree | 80cfe417dd9ab01b68038cdca9f2f9e67f16dcfa /parsing/g_tactic.ml4 | |
| parent | 7422420fb651d0bcbdf31d30ec93403460420daf (diff) | |
New tactics : econstructor, eleft, eright, esplit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4929 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 9c450101b..01b59dcf6 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -62,8 +62,8 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2) if !Options.v7 then GEXTEND Gram - GLOBAL: simple_tactic constrarg constr_with_bindings quantified_hypothesis - red_expr int_or_var castedopenconstr; + GLOBAL: simple_tactic constrarg with_bindings constr_with_bindings + quantified_hypothesis red_expr int_or_var castedopenconstr; int_or_var: [ [ n = integer -> Genarg.ArgArg n @@ -161,9 +161,9 @@ GEXTEND Gram ImplicitBindings (c1 :: bl) ] ] ; constr_with_bindings: - [ [ c = constr; l = with_binding_list -> (c, l) ] ] + [ [ c = constr; l = with_bindings -> (c, l) ] ] ; - with_binding_list: + with_bindings: [ [ "with"; bl = binding_list -> bl | -> NoBindings ] ] ; unfold_occ: @@ -343,12 +343,12 @@ GEXTEND Gram id2 = id_or_ltac_ref -> TacRename (id1,id2) (* Constructors *) - | IDENT "Left"; bl = with_binding_list -> TacLeft bl - | IDENT "Right"; bl = with_binding_list -> TacRight bl - | IDENT "Split"; bl = with_binding_list -> TacSplit (false,bl) + | IDENT "Left"; bl = with_bindings -> TacLeft bl + | IDENT "Right"; bl = with_bindings -> TacRight bl + | IDENT "Split"; bl = with_bindings -> TacSplit (false,bl) | IDENT "Exists"; bl = binding_list -> TacSplit (true,bl) | IDENT "Exists" -> TacSplit (true,NoBindings) - | IDENT "Constructor"; n = num_or_meta; l = with_binding_list -> + | IDENT "Constructor"; n = num_or_meta; l = with_bindings -> TacConstructor (n,l) | IDENT "Constructor"; t = OPT tactic -> TacAnyConstructor t |