diff options
| author | herbelin | 2003-11-01 22:24:32 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-01 22:24:32 +0000 |
| commit | 9b194e0a6588b58c1e54ac30f625e03deb378312 (patch) | |
| tree | 33af3c10f61e71f9f6460e2bd741c81e258e704e | |
| parent | 50d21e5c4f9613a2080d71925dd3a747aed70f5d (diff) | |
Pas de defaut a 1 et LeftA pour les infixes v8; fusion de l'univers et du nom d'entree en un 'Print Grammar entry' en v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4757 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/metasyntax.ml | 23 |
1 files changed, 17 insertions, 6 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 5960bbc049..2ccdfdc40b 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -204,10 +204,21 @@ let add_tactic_grammar g = (* printing grammar entries *) let print_grammar univ entry = - let u = get_univ univ in - let typ = explicitize_entry (fst u) entry in - let te,_,_ = get_constr_entry typ in - Gram.Entry.print te + if !Options.v7 then + let u = get_univ univ in + let typ = explicitize_entry (fst u) entry in + 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 + | "tuple_constr" -> weaken_entry Pcoq.Constr.tuple_constr + | "pattern" -> weaken_entry Pcoq.Constr.pattern + | "tuple_pattern" -> weaken_entry Pcoq.Constr.tuple_pattern + | "tactic" -> weaken_entry Pcoq.Tactic.simple_tactic + | _ -> error "Unknown or unprintable grammar entry" in + Gram.Entry.print te (* Parse a format *) let parse_format (loc,str) = @@ -1160,8 +1171,8 @@ let add_infix local (inf,modl) pr mv8 sc = onlyparse false else (* Infix defaults to LEFTA in V7 (cf doc) *) - let mv = match n with None -> SetLevel 1 :: modl | _ -> modl in - let mv = match assoc with None -> SetAssoc Gramext.LeftA :: mv | _ -> mv in + let mv = match n with None when !Options.v7 -> SetLevel 1 :: modl | _ -> modl in + let mv = match assoc with None when !Options.v7 -> SetAssoc Gramext.LeftA :: mv | _ -> mv in let mv8 = match mv8 with None -> None | Some(s8,mv8) -> |