diff options
| author | msozeau | 2011-11-18 14:02:22 +0000 |
|---|---|---|
| committer | msozeau | 2011-11-18 14:02:22 +0000 |
| commit | ec0c502f5c6920c2fd59a926c9de050cdf7780e1 (patch) | |
| tree | 1bd8392352aeeaa235ffd1941a1fb903acd3144b /pretyping/typeclasses.ml | |
| parent | 70e59380e6a6fb6cc5b4685159c2311929bb7b14 (diff) | |
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
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 16 |
1 files changed, 14 insertions, 2 deletions
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 = |