A much better implementation of implicit generalization:

- Do it after internalisation (esp. after notation expansion)
- Generalize it to any constr, not just typeclasses
- Prepare for having settings on the implicit status of generalized
variables (currently only impl,impl and expl,expl are supported).
- Simplified implementation! (Still some refactoring needed in
typeclasses parsing code).
This patch contains a fix for bug #1964 as well.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11490 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 7 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index e906fb3983..239d3772f0 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -205,17 +205,23 @@ let begin_of_binders = function
   | b::_ -> begin_of_binder b
   | _ -> 0
 
-let surround_binder k p = 
+let surround_impl k p = 
   match k with
-      Default Explicit -> hov 1 (str"(" ++ p ++ str")")
-    | Default Implicit -> hov 1 (str"{" ++ p ++ str"}")
-    | TypeClass _ -> hov 1 (str"[" ++ p ++ str"]")
+  | Explicit -> str"(" ++ p ++ str")"
+  | Implicit -> str"{" ++ p ++ str"}"
 
+let surround_binder k p = 
+  match k with
+  | Default b -> hov 1 (surround_impl b p)
+  | Generalized (b, b', t) -> 
+      hov 1 (surround_impl b' (surround_impl b p))
+	
 let surround_implicit k p =
   match k with
-      Default Explicit -> p
-    | Default Implicit -> (str"{" ++ p ++ str"}")
-    | TypeClass _ -> (str"[" ++ p ++ str"]")
+  | Default Explicit -> p
+  | Default Implicit -> (str"{" ++ p ++ str"}")
+  | Generalized (b, b', t) -> 
+      surround_impl b' (surround_impl b p)
 
 let pr_binder many pr (nal,k,t) =
   match t with