From ff03e8dd0de507be82e58ed5e8fd902dfd7caf4b Mon Sep 17 00:00:00 2001
From: msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 4 Jul 2008 14:38:44 +0000
Subject: Fixes in handling of implicit arguments: - Now [ id : Class foo ]
 makes id an explicit argument,   and [ Class foo ] is equivalent to [
 {someid} : Class foo ].   This makes declarations such as "Class Ord [ eq :
 Eq a ]" have   sensible implicit args. - Better handling of {} in class and
 record declarations, refactorize   code for declaring structures and classes.
 - Fix merging of implicit arguments information on section closing.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11204 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_constr.ml4 | 16 +++++++++-------
 parsing/pcoq.mli     |  2 +-
 parsing/ppconstr.ml  |  4 ++--
 parsing/q_coqast.ml4 |  2 +-
 4 files changed, 13 insertions(+), 11 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 6b6b4871c..3f437721a 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -409,17 +409,19 @@ GEXTEND Gram
   ;
   typeclass_constraint_binder:
     [ [ tc = typeclass_constraint ->
-      let (n,bk,t) = tc in
-	LocalRawAssum ([n], TypeClass bk, t)
+      let (n,(b,b'),t) = tc in
+	LocalRawAssum ([n], TypeClass (b,b'), t)
     ] ]
   ;
 
   typeclass_constraint:
-    [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), Explicit, c
-    | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
-	(loc, Name iid), expl, c
-    | c = operconstr LEVEL "200" ->
-	(loc, Anonymous), Implicit, c
+    [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), (Implicit, Explicit), c
+      | "{"; id = name; "}"; ":" ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
+	  id, (Implicit, expl), c
+      | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
+	  (loc, Name iid), (Explicit, expl), c
+      | c = operconstr LEVEL "200" ->
+	  (loc, Anonymous), (Implicit, Implicit), c
     ] ]
   ;
   
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index aaf4324e2..19cb28778 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -166,7 +166,7 @@ module Constr :
     val binder_let : local_binder list Gram.Entry.e
     val binders_let : local_binder list Gram.Entry.e
     val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
-    val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
+    val typeclass_constraint : (name located * (binding_kind * binding_kind) * constr_expr) Gram.Entry.e
     val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
   end
 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 04b700236..912406f3f 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -219,13 +219,13 @@ let surround_binder k p =
   match k with
       Default Explicit -> hov 1 (str"(" ++ p ++ str")")
     | Default Implicit -> hov 1 (str"{" ++ p ++ str"}")
-    | TypeClass b -> hov 1 (str"[" ++ p ++ str"]")
+    | TypeClass _ -> hov 1 (str"[" ++ p ++ str"]")
 
 let surround_implicit k p =
   match k with
       Default Explicit -> p
     | Default Implicit -> (str"{" ++ p ++ str"}")
-    | TypeClass b -> (str"[" ++ p ++ str"]")
+    | TypeClass _ -> (str"[" ++ p ++ str"]")
 
 let pr_binder many pr (nal,k,t) =
   match t with
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index e27a93b33..6bd795ed5 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -139,7 +139,7 @@ let mlexpr_of_binding_kind = function
 
 let mlexpr_of_binder_kind = function
   | Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >>
-  | Topconstr.TypeClass b -> <:expr< Topconstr.TypeClass $mlexpr_of_binding_kind b$ >>
+  | Topconstr.TypeClass (b,b') -> <:expr< Topconstr.TypeClass $mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_binding_kind (b,b')$ >>
 
 let rec mlexpr_of_constr = function
   | Topconstr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) ->
-- 
cgit v1.2.3