diff options
| author | herbelin | 2002-11-26 16:17:38 +0000 |
|---|---|---|
| committer | herbelin | 2002-11-26 16:17:38 +0000 |
| commit | aadcf42183225553b8e5dcf49685ecb59459af58 (patch) | |
| tree | 1ba2f2f69650f4cf1191bc16838a51b79795f228 /parsing/esyntax.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/esyntax.ml')
| -rw-r--r-- | parsing/esyntax.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml index 859b5548a5..1fa8523628 100644 --- a/parsing/esyntax.ml +++ b/parsing/esyntax.ml @@ -186,9 +186,8 @@ let pr_parenthesis inherited se strm = let print_delimiters inh se strm = function | None -> pr_parenthesis inh se strm - | Some sc -> - let (left,right) = out_some (find_delimiters sc) in - assert (left <> "" && right <> ""); + | Some key -> + let left = "`"^key^":" and right = "`" in let lspace = if is_letter (left.[String.length left -1]) then str " " else mt () in let rspace = |