diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-17 09:23:50 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-17 09:23:50 +0000 |
| commit | 6d42453dea17a8bd35530bf793344570ff9fc055 (patch) | |
| tree | d7ab7bd9934c0c48f80a3c3d88a1de8e20636f12 /toplevel/metasyntax.ml | |
| parent | 4f6a3a7968bfe6f6551f0f5902d3d76a7b69cd25 (diff) | |
Ajout de lconstr, constr et binder_constr dans Print Grammar constr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5355 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 0ded5150d..50e3f6260 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -215,13 +215,21 @@ let print_grammar univ entry = let te,_,_ = get_constr_entry false typ in Gram.Entry.print te else - let te = - match entry with - | "constr" | "operconstr" -> weaken_entry Pcoq.Constr.operconstr - | "pattern" -> weaken_entry Pcoq.Constr.pattern - | "tactic" -> weaken_entry Pcoq.Tactic.simple_tactic - | _ -> error "Unknown or unprintable grammar entry" in - Gram.Entry.print te + match entry with + | "constr" | "operconstr" | "binder_constr" -> + msgnl (str "Entry constr is"); + Gram.Entry.print Pcoq.Constr.constr; + msgnl (str "and lconstr is"); + Gram.Entry.print Pcoq.Constr.lconstr; + msgnl (str "where binder_constr is"); + Gram.Entry.print Pcoq.Constr.binder_constr; + msgnl (str "and operconstr is"); + Gram.Entry.print Pcoq.Constr.operconstr; + | "pattern" -> + Gram.Entry.print Pcoq.Constr.pattern + | "tactic" -> + Gram.Entry.print Pcoq.Tactic.simple_tactic + | _ -> error "Unknown or unprintable grammar entry" (* Parse a format (every terminal starting with a letter or a single quote (except a single quote alone) must be quoted) *) |