From 3d09e39dd423d81c6af3e991d5b282ea8608646b Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 17 Jul 2013 15:31:36 +0000
Subject: More dynamic argument scopes

 When arguments scopes are set manually, nothing new, they stay
 as they are (until maybe another Arguments invocation).
 But when argument scopes are computed out of the argument type and
 the Bind Scope information, this kind of scope is now dynamic:
 a later Bind Scope will be able to impact the scopes of an earlier
 constant. For Instance:

 Definition f (n:nat) := n.
 About f. (* Argument scope is [nat_scope] *)
 Bind Scope other_scope with nat.
 About f. (* Argument scope is [other_scope] *)

 This allows to get rid of hacks for modifying scopes during functor
 applications. Moreover, the subst_arguments_scope is now
 environment-insensitive (needed for forthcoming changes in declaremods).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16626 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 printing/ppvernac.ml | 22 +++++++---------------
 1 file changed, 7 insertions(+), 15 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index d8ddb275d1..3c4f25880b 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -222,21 +222,13 @@ let rec pr_module_ast pr_c = function
       pr_module_ast pr_c me1 ++ spc() ++
       hov 1 (str"(" ++ pr_module_ast pr_c me2 ++ str")")
 
-let pr_annot { ann_inline = ann; ann_scope_subst = scl } =
-  let sep () = if List.is_empty scl then mt () else str "," in
-  if ann == DefaultInline && List.is_empty scl then mt ()
-  else
-    str " [" ++
-    (match ann with
-      | DefaultInline -> mt ()
-      | NoInline -> str "no inline" ++ sep ()
-      | InlineAt i -> str "inline at level " ++ int i ++ sep ()) ++
-    prlist_with_sep (fun () -> str ", ")
-      (fun (sc1,sc2) -> str ("scope "^sc1^" to "^sc2)) scl ++
-    str "]"
-
-let pr_module_ast_inl pr_c (mast,ann) =
-  pr_module_ast pr_c mast ++ pr_annot ann
+let pr_inline = function
+  | DefaultInline -> mt ()
+  | NoInline -> str "[no inline]"
+  | InlineAt i -> str "[inline at level " ++ int i ++ str "]"
+
+let pr_module_ast_inl pr_c (mast,inl) =
+  pr_module_ast pr_c mast ++ pr_inline inl
 
 let pr_of_module_type prc = function
   | Enforce mty -> str ":" ++ pr_module_ast_inl prc mty
-- 
cgit v1.2.3