diff options
| author | delahaye | 2002-03-17 04:57:32 +0000 |
|---|---|---|
| committer | delahaye | 2002-03-17 04:57:32 +0000 |
| commit | 1a750105e7d9630acf44dd0833cdc34578a0aea5 (patch) | |
| tree | 5165a4abf83dec76bca5fc37fdc1403e23c0bb58 /parsing | |
| parent | 6e616fea2b9e153b04232537b7ee2539409521ac (diff) | |
Meilleure gestion de la reduction dans Field
Field term (nouveau)
Injections dans l'interpreteur de tactiques
Exportation de quelques entrees de grammaires
Exportation de quelques fonctionnalites des definitions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2538 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 5 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
4 files changed, 7 insertions, 4 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index a64ebb8268..b90924f81a 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -21,7 +21,7 @@ open Util (* Tactics grammar rules *) GEXTEND Gram - GLOBAL: tactic_expr input_fun; + GLOBAL: tactic_atom tactic_atom0 tactic_expr input_fun; input_fun: [ [ l = identarg -> l | "()" -> <:ast< (VOID) >> ] ] @@ -144,7 +144,8 @@ GEXTEND Gram | IDENT "Inst"; id = identarg; "["; c = Constr.constr; "]" -> <:ast< (COMMAND (CONTEXT $id $c)) >> | st = simple_tactic -> st - | id = lqualid; la = LIST1 tactic_atom0 -> <:ast< (APP $id ($LIST $la)) >> + | id = lqualid; la = LIST1 tactic_atom0 -> + <:ast< (APP $id ($LIST $la)) >> | id = lqualid -> id | ta = tactic_atom0 -> ta ] ] ; diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 0c2a618965..a864227a71 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -51,7 +51,7 @@ END (* Gallina declarations *) GEXTEND Gram - GLOBAL: gallina gallina_ext thm_tok theorem_body; + GLOBAL: gallina gallina_ext reduce thm_tok theorem_body; theorem_body_line: [ [ n = numarg; ":"; tac = tacarg; "." -> @@ -105,7 +105,7 @@ GEXTEND Gram ; reduce: [ [ IDENT "Eval"; r = Tactic.red_tactic; "in" -> - [ <:ast< (TACTIC_ARG (REDEXP $r)) >> ] + [ <:ast< (TACTIC_ARG (REDEXP $r)) >> ] | -> [] ] ] ; binders_list: diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index ffa82f0342..c45c8227d6 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -371,6 +371,7 @@ module Vernac_ = let constrarg = gec "constrarg" let ne_constrarg_list = gec_list "ne_constrarg_list" let tacarg = gec "tacarg" + let reduce = gec_list "reduce" let sortarg = gec "sortarg" let theorem_body = gec "theorem_body" let thm_tok = gec "thm_tok" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 3b55171b72..781c651621 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -181,6 +181,7 @@ module Vernac_ : val constrarg : Coqast.t Gram.Entry.e val ne_constrarg_list : Coqast.t list Gram.Entry.e val tacarg : Coqast.t Gram.Entry.e + val reduce : Coqast.t list Gram.Entry.e val sortarg : Coqast.t Gram.Entry.e val theorem_body : Coqast.t Gram.Entry.e val thm_tok : Coqast.t Gram.Entry.e |