diff options
| author | herbelin | 2006-03-05 09:05:12 +0000 |
|---|---|---|
| committer | herbelin | 2006-03-05 09:05:12 +0000 |
| commit | ec0999d90b7bce9c0f61300be7bc3e0016f12fbf (patch) | |
| tree | 76c8daa922456751cb6fc839ce32ea77031fc462 | |
| parent | 46a26794042f93ef3892b52208d2167c5ec71de4 (diff) | |
Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une référence explicitement de ltac + suppression de la répétition de l'entrée 'reference' dans tactic_atom
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8129 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_ltac.ml4 | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 1deffe6d35..60a00df3df 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -35,6 +35,11 @@ let arg_of_expr = function TacArg a -> a | e -> Tacexp (e:raw_tactic_expr) +let tacarg_of_expr = function + | TacArg (Reference r) -> TacCall (dummy_loc,r,[]) + | TacArg a -> a + | e -> Tacexp (e:raw_tactic_expr) + (* Tactics grammar rules *) GEXTEND Gram @@ -101,9 +106,10 @@ GEXTEND Gram ; (* Tactic arguments *) tactic_arg: - [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a + [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> tacarg_of_expr a | IDENT "ipattern"; ":"; ipat = simple_intropattern -> IntroPattern ipat | a = may_eval_arg -> a + | r = reference -> Reference r | a = tactic_atom -> a | c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ] ; @@ -125,7 +131,6 @@ GEXTEND Gram ; tactic_atom: [ [ id = METAIDENT -> MetaIdArg (loc,id) - | r = reference -> Reference r | "()" -> TacVoid ] ] ; match_key: |