From ec0c502f5c6920c2fd59a926c9de050cdf7780e1 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 18 Nov 2011 14:02:22 +0000
Subject: 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
---
 pretyping/typeclasses.ml  | 16 ++++++++++++++--
 pretyping/typeclasses.mli |  4 +++-
 2 files changed, 17 insertions(+), 3 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3