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, 8 insertions, 8 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 740ba0b34..5f729762f 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -399,11 +399,11 @@ GEXTEND Gram
     | "{"; id=name; idl=LIST1 name; "}" -> 
         List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
     | "("; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; ")" ->
-	List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Explicit, b), t)) tc
+	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Explicit, Explicit, b), t)) tc
     | "{"; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; "}" ->
-	List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Implicit, b), t)) tc
-    | "["; tc = LIST1 typeclass_constraint SEP ","; "]" -> 
-	List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Implicit, b), t)) tc
+	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
+    | "["; tc = LIST1 typeclass_constraint SEP ","; "]" ->
+	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
     ] ]
   ;
   binder:
@@ -413,13 +413,13 @@ GEXTEND Gram
     ] ]
   ;
   typeclass_constraint:
-    [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), Explicit, c
-      | "{"; id = name; "}"; ":" ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
+    [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), true, c
+      | "{"; id = name; "}"; ":" ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
 	  id, expl, c
-      | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
+      | iid=ident_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
 	  (loc, Name iid), expl, c
       | c = operconstr LEVEL "200" ->
-	  (loc, Anonymous), Implicit, c
+	  (loc, Anonymous), false, c
     ] ]
   ;