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

8 files changed, 54 insertions, 26 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
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d79310d109..e85f174e0e 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -47,6 +47,7 @@ let resolve_one_typeclass env evm t =
   !solve_instanciation_problem env evm t
 
 type rels = constr list
+type direction = Forward | Backward
 
 (* This module defines type-classes *)
 type typeclass = {
@@ -60,7 +61,7 @@ type typeclass = {
   cl_props : rel_context;
 
   (* The method implementaions as projections. *)
-  cl_projs : (name * int option option * constant option) list;
+  cl_projs : (name * (direction * int option) option * constant option) list;
 }
 
 module Gmap = Fmap.Make(RefOrdered)
@@ -251,7 +252,8 @@ let build_subclasses ~check env sigma glob pri =
 	  (fun (n, b, proj) ->
 	   match b with 
 	   | None -> None
-	   | Some pri' ->
+	   | Some (Backward, _) -> None
+	   | Some (Forward, pri') ->
 	     let proj = Option.get proj in
 	     let body = it_mkLambda_or_LetIn (mkApp (mkConst proj, projargs)) rels in
 	       if check && check_instance env sigma body then None
@@ -364,6 +366,16 @@ let declare_instance pri local glob =
 (* 	(Auto.HintsCutEntry (PathSeq (PathStar (PathAtom PathAny), path))) *)
     | None -> ()
 
+let add_class cl =
+  add_class cl;
+  List.iter (fun (n, inst, body) ->
+	     match inst with
+	     | Some (Backward, pri) ->
+	       declare_instance pri false (ConstRef (Option.get body))
+	     | _ -> ())
+  cl.cl_projs
+
+
 open Declarations
 
 let add_constant_class cst =
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index a00d23a9b2..74ccaf834f 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -18,6 +18,8 @@ open Mod_subst
 open Topconstr
 open Util
 
+type direction = Forward | Backward
+
 (** This module defines type-classes *)
 type typeclass = {
   (** The class implementation: a record parameterized by the context with defs in it or a definition if
@@ -36,7 +38,7 @@ type typeclass = {
       Some may be undefinable due to sorting restrictions or simply undefined if 
       no name is provided. The [int option option] indicates subclasses whose hint has
       the given priority. *)
-  cl_projs : (name * int option option * constant option) list;
+  cl_projs : (name * (direction * int option) option * constant option) list;
 }
 
 type instance
diff --git a/toplevel/record.ml b/toplevel/record.ml
index a7f7b24588..ee190d3506 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -334,7 +334,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
 	Classes.set_typeclass_transparency (EvalConstRef cst) false false;
 	if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign ();
-	let sub = if List.hd coers then Some (List.hd priorities) else None in
+	let sub = match List.hd coers with Some b -> Some ((if b then Backward else Forward), List.hd priorities) | None -> None in
 	  cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
 	let idarg = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
@@ -342,7 +342,10 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	  params (Option.default (Termops.new_Type ()) arity) fieldimpls fields
 	  ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign
 	in
-	let coers = List.map2 (fun coe pri -> if coe then Some pri else None) coers priorities in
+	let coers = List.map2 (fun coe pri -> 
+			       Option.map (fun b -> if b then Backward, pri else Forward, pri) coe) 
+	  coers priorities 
+	in
 	  IndRef ind, (list_map3 (fun (id, _, _) b y -> (id, b, y))
 			 (List.rev fields) coers (Recordops.lookup_projections ind))
   in
@@ -374,8 +377,9 @@ let interp_and_check_sort sort =
 open Vernacexpr
 open Autoinstance
 
-(* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean
-   list telling if the corresponding fields must me declared as coercion *)
+(* [fs] corresponds to fields and [ps] to parameters; [coers] is a
+   list telling if the corresponding fields must me declared as coercions 
+   or subinstances *)
 let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) =
   let cfs,notations = List.split cfs in
   let cfs,priorities = List.split cfs in
@@ -404,6 +408,7 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil
 	let arity = Option.default (Termops.new_Type ()) sc in
 	let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in
-	let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs fields is_coe coers sign in
+	let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs 
+	  fields is_coe (List.map (fun coe -> coe <> None) coers) sign in
 	if infer then search_record declare_record_instance (ConstructRef (ind,1)) sign;
 	IndRef ind
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 131a5b9e1f..45670f1fae 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -20,7 +20,7 @@ open Libnames
 
 val declare_projections :
   inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
-  bool list -> manual_explicitation list list -> rel_context ->
+  coercion_flag list -> manual_explicitation list list -> rel_context ->
   (name * bool) list * constant option list
 
 val declare_structure : Decl_kinds.recursivity_kind ->
@@ -35,5 +35,5 @@ val declare_structure : Decl_kinds.recursivity_kind ->
 
 val definition_structure :
   inductive_kind * Decl_kinds.recursivity_kind * bool(**infer?*)* lident with_coercion * local_binder list *
-  (local_decl_expr with_coercion with_priority with_notation) list *
+  (local_decl_expr with_instance with_priority with_notation) list *
   identifier * constr_expr option -> global_reference
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 07454337f7..cd30eaf5ca 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -415,7 +415,8 @@ let vernac_inductive finite infer indl =
   | [ ( id , bl , c , Class true, Constructors [l]), _ ] ->
       let f =
 	let (coe, ((loc, id), ce)) = l in
-	  (((coe, AssumExpr ((loc, Name id), ce)), None), [])
+	let coe' = if coe then Some false else None in
+	  (((coe', AssumExpr ((loc, Name id), ce)), None), [])
       in vernac_record (Class true) finite infer id bl c None [f]
   | [ ( id , bl , c , Class true, _), _ ] ->
       Util.error "Definitional classes must have a single method"
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index ea7d0c6e2f..32ea70baf2 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -125,7 +125,8 @@ type rec_flag       = bool (* true = Rec;           false = NoRec          *)
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
 type opacity_flag   = bool (* true = Opaque;        false = Transparent    *)
 type locality_flag  = bool (* true = Local;         false = Global         *)
-type coercion_flag  = bool (* true = AddCoercion;   false = NoCoercion     *)
+type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
+type instance_flag  = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
 type export_flag    = bool (* true = Export;        false = Import         *)
 type specif_flag    = bool (* true = Specification; false = Implementation *)
 type inductive_flag = Decl_kinds.recursivity_kind
@@ -164,12 +165,13 @@ type decl_notation = lstring * constr_expr * scope_name option
 type simple_binder = lident list  * constr_expr
 type class_binder = lident * constr_expr list
 type 'a with_coercion = coercion_flag * 'a
+type 'a with_instance = instance_flag * 'a
 type 'a with_notation = 'a * decl_notation list
 type 'a with_priority = 'a * int option
 type constructor_expr = (lident * constr_expr) with_coercion
 type constructor_list_or_record_decl_expr =
   | Constructors of constructor_expr list
-  | RecordDecl of lident option * local_decl_expr with_coercion with_priority with_notation list
+  | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list
 type inductive_expr =
   lident with_coercion * local_binder list * constr_expr option * inductive_kind *
     constructor_list_or_record_decl_expr