diff options
author | 2003-03-28 17:25:57 +0000 | |
---|---|---|
committer | 2003-03-28 17:25:57 +0000 | |
commit | e123d91faac12f9d304e7b245365ce5326e77f7a (patch) | |
tree | f9cf16d5b1ab582baa3c842f88fcb692dd72a343 /parsing/printer.ml | |
parent | 4fb5ef358e3e0fbfad378ea5037fea6dafd5e27a (diff) |
notations <>, Assumption avec existentiel, replace term
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3802 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/printer.ml')
-rw-r--r-- | parsing/printer.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index df2aabdf8..1c19352b2 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -148,7 +148,7 @@ let pr_var_decl env (id,c,typ) = | Some c -> (* Force evaluation *) let pb = prterm_env env c in - (str" := " ++ pb) in + (str" := " ++ pb ++ cut () ) in let pt = prtype_env env typ in let ptyp = (str" : " ++ pt) in (pr_id id ++ hov 0 (pbody ++ ptyp)) |