Restore backward compatibility. ":>" declares subinstances in Class declarations, in the usual backward mode,

the new token ":>>" declares the subinstance as a forward hint.
Both declare a coercion in other contexts. Cleanup the code for declarations for less confusion between
coercions and subinstance hints.

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

2 files changed, 19 insertions, 13 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 07e0d5b5ab..5fe558adf1 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -344,12 +344,12 @@ GEXTEND Gram
       | l = binders; ":="; b = lconstr -> fun id ->
          match b with
 	 | CCast(_,b, Glob_term.CastConv (_, t)) ->
-	     (false,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t)))
+	     (None,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t)))
          | _ ->
-	     (false,DefExpr(id,mkCLambdaN loc l b,None)) ] ]
+	     (None,DefExpr(id,mkCLambdaN loc l b,None)) ] ]
   ;
   record_binder:
-    [ [ id = name -> (false,AssumExpr(id,CHole (loc, None)))
+    [ [ id = name -> (None,AssumExpr(id,CHole (loc, None)))
       | id = name; f = record_binder_body -> f id ] ]
   ;
   assum_list:
@@ -360,13 +360,13 @@ GEXTEND Gram
   ;
   simple_assum_coe:
     [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr ->
-        (oc,(idl,c)) ] ]
+        (oc <> None,(idl,c)) ] ]
   ;
 
   constructor_type:
     [[ l = binders;
       t= [ coe = of_type_with_opt_coercion; c = lconstr ->
-	            fun l id -> (coe,(id,mkCProdN loc l c))
+	            fun l id -> (coe <> None,(id,mkCProdN loc l c))
             |  ->
 		 fun l id -> (false,(id,mkCProdN loc l (CHole (loc, None)))) ]
 	 -> t l
@@ -377,9 +377,11 @@ GEXTEND Gram
     [ [ id = identref; c=constructor_type -> c id ] ]
   ;
   of_type_with_opt_coercion:
-    [ [ ":>" -> true
-      | ":"; ">" -> true
-      | ":" -> false ] ]
+    [ [ ":>>" -> Some false
+    | ":>" -> Some true
+    | ":"; ">" -> Some true
+    | ":"; ">"; ">" -> Some false
+    | ":" -> None ] ]
   ;
 END
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 5435a98720..9500130130 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -428,18 +428,22 @@ let make_pr_vernac pr_constr pr_lconstr =
 let pr_constrarg c = spc () ++ pr_constr c in
 let pr_lconstrarg c = spc () ++ pr_lconstr c in
 let pr_intarg n = spc () ++ int n in
-(* let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in *)
+let pr_oc = function 
+    None -> str" :"
+  | Some true -> str" :>"
+  | Some false -> str" :>>"
+in
 let pr_record_field ((x, pri), ntn) =
   let prx = match x with
     | (oc,AssumExpr (id,t)) ->
 	hov 1 (pr_lname id ++
-		  (if oc then str" :>" else str" :") ++ spc() ++
-		  pr_lconstr_expr t)
+	       pr_oc oc ++ spc() ++
+	       pr_lconstr_expr t)
     | (oc,DefExpr(id,b,opt)) -> (match opt with
       | Some t ->
           hov 1 (pr_lname id ++
-                    (if oc then str" :>" else str" :") ++ spc() ++
-                    pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
+                 pr_oc oc ++ spc() ++
+                 pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
       | None ->
           hov 1 (pr_lname id ++ str" :=" ++ spc() ++
                     pr_lconstr b)) in