diff options
| author |  clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-01 15:36:05 +0000 |
|---|---|---|
| committer | clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-01 15:36:05 +0000 |
| commit | 34f26b527c2bec59ed496760329603b20ea6e332 (patch) | |
| tree | f597ca512ec79d102d0c62d377d05eedbe34d87c /parsing/g_tactic.ml4 | |
| parent | 1d5d6427e6ab85f925207ee099729932c669ab16 (diff) | |
Nouvelle tactique EExists
Changement des exports pour tactic EXTEND : with_bindings devient bindings qui prend plus le with, il faut le mettre à la main dans la règle.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5052 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 2416b14bd..cf10f0c45 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -62,7 +62,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2) if !Options.v7 then GEXTEND Gram - GLOBAL: simple_tactic constrarg with_bindings constr_with_bindings + GLOBAL: simple_tactic constrarg bindings constr_with_bindings quantified_hypothesis red_expr int_or_var castedopenconstr; int_or_var: @@ -151,7 +151,7 @@ GEXTEND Gram [ [ id = base_ident; ":="; c = constr -> (loc, NamedHyp id, c) | n = natural; ":="; c = constr -> (loc, AnonHyp n, c) ] ] ; - binding_list: + bindings: [ [ c1 = constr; ":="; c2 = constr; bl = LIST0 simple_binding -> ExplicitBindings ((join_to_constr loc c2,NamedHyp (coerce_to_id c1), c2) :: bl) @@ -164,7 +164,7 @@ GEXTEND Gram [ [ c = constr; l = with_bindings -> (c, l) ] ] ; with_bindings: - [ [ "with"; bl = binding_list -> bl | -> NoBindings ] ] + [ [ "with"; bl = bindings -> bl | -> NoBindings ] ] ; unfold_occ: [ [ nl = LIST0 integer; c = global_or_ltac_ref -> (nl,c) ] ] @@ -346,7 +346,7 @@ GEXTEND Gram | 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"; bl = bindings -> TacSplit (true,bl) | IDENT "Exists" -> TacSplit (true,NoBindings) | IDENT "Constructor"; n = num_or_meta; l = with_bindings -> TacConstructor (n,l) |