From 9cf6b3543bf369ccb4d3b0909ee3db96e074e24e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 10 Feb 2010 00:14:07 +0000
Subject: 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
---
 pretyping/typeclasses.ml | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

(limited to 'pretyping/typeclasses.ml')

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