From 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Thu, 19 Jan 2006 22:34:29 +0000 Subject: Imported Upstream version 8.0pl3 --- parsing/g_ltacnew.ml4 | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) (limited to 'parsing/g_ltacnew.ml4') diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index 9c8d1675..7492ac8c 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: g_ltacnew.ml4,v 1.22.2.2 2004/07/16 19:30:38 herbelin Exp $ *) +(* $Id: g_ltacnew.ml4,v 1.22.2.3 2005/06/21 15:31:12 herbelin Exp $ *) open Pp open Util @@ -43,7 +43,7 @@ let tactic_expr = Gram.Entry.create "tactic:tactic_expr" if not !Options.v7 then GEXTEND Gram - GLOBAL: tactic Vernac_.command tactic_expr tactic_arg; + GLOBAL: tactic Vernac_.command tactic_expr tactic_arg constr_may_eval; tactic_expr: [ "5" LEFTA @@ -108,14 +108,20 @@ GEXTEND Gram | c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ] ; may_eval_arg: + [ [ c = constr_eval -> ConstrMayEval c + | IDENT "fresh"; s = OPT STRING -> TacFreshId s ] ] + ; + constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> - ConstrMayEval (ConstrEval (rtc,c)) + ConstrEval (rtc,c) | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" -> - ConstrMayEval (ConstrContext (id,c)) + ConstrContext (id,c) | IDENT "type"; IDENT "of"; c = Constr.constr -> - ConstrMayEval (ConstrTypeOf c) - | IDENT "fresh"; s = OPT STRING -> - TacFreshId s ] ] + ConstrTypeOf c ] ] + ; + constr_may_eval: (* For extensions *) + [ [ c = constr_eval -> c + | c = Constr.constr -> ConstrTerm c ] ] ; tactic_atom: [ [ id = METAIDENT -> MetaIdArg (loc,id) -- cgit v1.2.3