diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /parsing/g_ltac.ml4 | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'parsing/g_ltac.ml4')
-rw-r--r-- | parsing/g_ltac.ml4 | 27 |
1 files changed, 12 insertions, 15 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index dac4a135..d082b91c 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -1,29 +1,26 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4use: "pa_extend.cmo" i*) - -(* $Id: g_ltac.ml4 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Topconstr -open Rawterm +open Glob_term open Tacexpr open Vernacexpr open Pcoq open Prim open Tactic +open Tok let fail_default_value = ArgArg 0 let arg_of_expr = function - TacArg a -> a + TacArg (loc,a) -> a | e -> Tacexp (e:raw_tactic_expr) (* Tactics grammar rules *) @@ -60,6 +57,7 @@ GEXTEND Gram | "3" RIGHTA [ IDENT "try"; ta = tactic_expr -> TacTry ta | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta) + | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta) | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta | IDENT "progress"; ta = tactic_expr -> TacProgress ta (*To do: put Abstract in Refiner*) @@ -82,25 +80,24 @@ GEXTEND Gram TacFirst l | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> TacSolve l - | IDENT "complete" ; ta = tactic_expr -> TacComplete ta | IDENT "idtac"; l = LIST0 message_token -> TacId l | IDENT "fail"; n = [ n = int_or_var -> n | -> fail_default_value ]; l = LIST0 message_token -> TacFail (n,l) | IDENT "external"; com = STRING; req = STRING; la = LIST1 tactic_arg -> - TacArg (TacExternal (loc,com,req,la)) + TacArg (loc,TacExternal (loc,com,req,la)) | st = simple_tactic -> TacAtom (loc,st) - | a = may_eval_arg -> TacArg(a) + | a = may_eval_arg -> TacArg(loc,a) | IDENT "constr"; ":"; id = METAIDENT -> - TacArg(MetaIdArg (loc,false,id)) + TacArg(loc,MetaIdArg (loc,false,id)) | IDENT "constr"; ":"; c = Constr.constr -> - TacArg(ConstrMayEval(ConstrTerm c)) + TacArg(loc,ConstrMayEval(ConstrTerm c)) | IDENT "ipattern"; ":"; ipat = simple_intropattern -> - TacArg(IntroPattern ipat) + TacArg(loc,IntroPattern ipat) | r = reference; la = LIST0 tactic_arg -> - TacArg(TacCall (loc,r,la)) ] + TacArg(loc,TacCall (loc,r,la)) ] | "0" [ "("; a = tactic_expr; ")" -> a - | a = tactic_atom -> TacArg a ] ] + | a = tactic_atom -> TacArg (loc,a) ] ] ; (* binder_tactic: level 5 of tactic_expr *) binder_tactic: |