From 483e36a76c4a31a1711a4602be45f66e7f46760f Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 11 Feb 2011 16:54:18 +0000
Subject: Annotations at functor applications:

 - The experimental syntax "<30>F M" is transformed into "F M [inline at level 30]"
 - The earlier syntax !F X should now be written "F X [no inline]"
   (note that using ! is still possible for compatibility)
 - A new annotation "F M [scope foo_scope to bar_scope]" allow to substitute
   foo_scope by bar_scope in all arguments scope of objects in F.

 BigN and BigZ are cleaned from the zillions of Arguments Scope used earlier.
 Arguments scope for lemmas are fixed for instances of Numbers.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13839 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/printers.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 9403a4ccad..476e2111e8 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -90,6 +90,7 @@ Coercion
 Unification
 Cases
 Pretyping
+Declaremods
 
 Tok
 Lexer
-- 
cgit v1.2.3