summaryrefslogtreecommitdiff
path: root/parsing/g_tactic.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_tactic.ml4')
-rw-r--r--parsing/g_tactic.ml411
1 files changed, 7 insertions, 4 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 2e067215..a1559572 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: g_tactic.ml4,v 1.83.2.2 2004/07/16 19:30:39 herbelin Exp $ *)
+(* $Id: g_tactic.ml4,v 1.83.2.4 2005/01/15 14:56:53 herbelin Exp $ *)
open Pp
open Ast
@@ -42,7 +42,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
if !Options.v7 then
GEXTEND Gram
GLOBAL: simple_tactic constrarg bindings constr_with_bindings
- quantified_hypothesis red_expr int_or_var castedopenconstr
+ quantified_hypothesis red_expr int_or_var castedopenconstr open_constr
simple_intropattern;
int_or_var:
@@ -96,8 +96,11 @@ GEXTEND Gram
| IDENT "Check"; c = constr -> ConstrTypeOf c
| c = constr -> ConstrTerm c ] ]
;
+ open_constr:
+ [ [ c = constr -> ((),c) ] ]
+ ;
castedopenconstr:
- [ [ c = constr -> c ] ]
+ [ [ c = constr -> ((),c) ] ]
;
induction_arg:
[ [ n = natural -> ElimOnAnonHyp n
@@ -180,7 +183,7 @@ GEXTEND Gram
| IDENT "Unfold"; ul = LIST1 unfold_occ -> Unfold ul
| IDENT "Fold"; cl = LIST1 constr -> Fold cl
| IDENT "Pattern"; pl = LIST1 pattern_occ -> Pattern pl
- | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ]
+ | s = IDENT -> ExtraRedExpr s ] ]
;
hypident:
[ [ id = id_or_meta -> id,[],(InHyp,ref None)