diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-26 16:17:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-26 16:17:38 +0000 |
| commit | aadcf42183225553b8e5dcf49685ecb59459af58 (patch) | |
| tree | 1ba2f2f69650f4cf1191bc16838a51b79795f228 /parsing/ppconstr.ml | |
| parent | 22c9662db9caef7fbb3f51d89e17fb4aa3d52646 (diff) | |
Réaffichage des Syntactic Definition (printer constr_expr).
Affinement de la gestion des niveaux de constr.
Cablage en dur du parsing et de l'affichage des délimiteurs de scopes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3295 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ppconstr.ml')
| -rw-r--r-- | parsing/ppconstr.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index e49f531f1..e177bb621 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -103,11 +103,8 @@ let pr_notation pr s env = let unpl, level = find_notation_printing_rule s in prlist (print_hunk pr env) unpl, level -let pr_delimiters sc strm = - match find_delimiters sc with - | None -> anomaly "Delimiters without concrete syntax" - | Some (left,right) -> - assert (left <> "" && right <> ""); +let pr_delimiters key strm = + let left = "`"^key^":" and right = "`" in let lspace = if is_letter (left.[String.length left -1]) then str " " else mt () in let rspace = |