diff options
| author | msozeau | 2010-02-10 00:14:07 +0000 |
|---|---|---|
| committer | msozeau | 2010-02-10 00:14:07 +0000 |
| commit | 9cf6b3543bf369ccb4d3b0909ee3db96e074e24e (patch) | |
| tree | 196dcb18bb968916f462705a5a2f606be24376f5 /pretyping/typeclasses.ml | |
| parent | c4b5c7ebd6f316bb53e1a53f94c367f4f0129dae (diff) | |
Fix [Existing Class] impl and add documentation. Fix computation of the
dependency order of obligations that was not backwards-compatible.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12719 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 94ade8c3c9..b85c672109 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -241,7 +241,7 @@ let add_constant_class cst = let ctx, arity = decompose_prod_assum ty in let tc = { cl_impl = ConstRef cst; - cl_context = ([], ctx); + cl_context = (List.map (const None) ctx, ctx); cl_props = [(Anonymous, None, arity)]; cl_projs = [] } @@ -251,18 +251,16 @@ let add_constant_class cst = let add_inductive_class ind = let mind, oneind = Global.lookup_inductive ind in let k = + let ctx = oneind.mind_arity_ctxt in let ty = Inductive.type_of_inductive_knowing_parameters - (push_rel_context oneind.mind_arity_ctxt (Global.env ())) - oneind (Termops.rel_vect 1 (List.length oneind.mind_arity_ctxt)) + (push_rel_context ctx (Global.env ())) + oneind (Termops.extended_rel_vect 0 ctx) in { cl_impl = IndRef ind; - cl_context = [], oneind.mind_arity_ctxt; + cl_context = List.map (const None) ctx, ctx; cl_props = [Anonymous, None, ty]; cl_projs = [] } - in add_class k; - Array.iteri (fun i _ -> - add_instance (new_instance k None true (ConstructRef (ind, succ i)))) - oneind.mind_consnames + in add_class k (* * interface functions |