From 6497f27021fec4e01f2182014f2bb1989b4707f9 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Mon, 31 Jan 2005 14:34:14 +0000 Subject: Imported Upstream version 8.0pl2 --- parsing/g_tactic.ml4 | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'parsing/g_tactic.ml4') 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) -- cgit v1.2.3