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

8 files changed, 38 insertions, 35 deletions

diff --git a/CHANGES b/CHANGES
index b36dbb55c..a43ff34e4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -176,24 +176,24 @@ Language
 Program
 
 - Streamlined definitions using well-founded recursion and measures so
-  that they can work on any number subset of the arguments directly
-  (uses currying).
+  that they can work on any subset of the arguments directly (uses currying).
 - Try to automatically clear structural fixpoint prototypes in
-  obligations to avoid issues of opacity.
-- Use return type clause inference as in the standard typing algorithm.
+  obligations to avoid issues with opacity.
+- Use return type clause inference in pattern-matching as in the standard 
+  typing algorithm.
 - Support [Local Obligation Tactic] and [Next Obligation with tactic].
 - Use [Show Obligation Tactic] to print the current default tactic.
 - [fst] and [snd] have maximal implicits in Program now (possible source
-  of incompatibility)
+  of incompatibility).
 
 Typeclasses
 
 - Use [Existing Class foo] to declare foo as a class a posteriori.
-  [foo] can be an inductive type or a constant definition, no
-  projections are defined.
+  [foo] can be an inductive type or a constant definition. No
+  projections or instances are defined.
 - Various bug fixes and improvements: support for defined fields, 
   anonymous instances, declarations giving terms, better handling of
-  sections, contexts.
+  sections and [Context].
 
 
 Changes from V8.1 to V8.2
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 1ea07f79a..7bd4f3522 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -305,6 +305,10 @@ parameters {\binder$_1$} to {\binder$_n$} and fields {\tt field$_1$} to
   proof size by not inserting useless projections. The class
   constant itself is declared rigid during resolution so that the class 
   abstraction is maintained.  
+
+\item \label{ExistingClass} {\tt Existing Class {\ident}.\comindex{Existing Class}}
+  This variant declares a class a posteriori from a constant or
+  inductive definition. No methods or instances are defined.
 \end{Variants}
 
 \subsection{\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} :
diff --git a/lib/util.ml b/lib/util.ml
index b8ceea3ea..8512e10e1 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1126,6 +1126,8 @@ let identity x = x
 
 let compose f g x = f (g x)
 
+let const x _ = x
+
 let iterate f =
   let rec iterate_f n x =
     if n <= 0 then x else iterate_f (pred n) (f x)
diff --git a/lib/util.mli b/lib/util.mli
index 7784635c3..ddf32e762 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -262,6 +262,7 @@ val matrix_transpose : 'a list list -> 'a list list
 
 val identity : 'a -> 'a
 val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
+val const : 'a -> 'b -> 'a
 val iterate : ('a -> 'a) -> int -> 'a -> 'a
 val repeat : int -> ('a -> unit) -> 'a -> unit
 val iterate_for : int -> int -> (int -> 'a -> 'a) -> 'a -> 'a
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index d9b73109a..4b95df197 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -143,21 +143,14 @@ let evar_dependencies evm ev =
   in aux (Intset.singleton ev)
 
 let sort_dependencies evl =
-  let one_step deps ine oute =
-    List.fold_left (fun (ine, oute, acc) (id, _, deps' as d) -> 
-      if not (Intset.mem id deps) then
-	if Intset.subset deps' (Intset.add id deps) then
-	  (d :: ine, oute, Intset.add id acc)
-	else (ine, d :: oute, acc)
-      else (ine, oute, acc))
-      (ine, [], deps) oute
-  in
-  let rec aux deps evsin evsout =
-    let (evsin, evsout, deps') = one_step deps evsin evsout in
-      if evsout = [] then List.rev evsin
-      else aux deps' evsin evsout
-  in aux Intset.empty [] evl
-
+  List.stable_sort
+    (fun (id, ev, deps) (id', ev', deps') ->
+      if id = id' then 0
+      else if Intset.mem id deps' then -1
+      else if Intset.mem id' deps then 1
+      else Pervasives.compare id id')
+    evl
+      
 let map_evar_body f = function
   | Evar_empty -> Evar_empty
   | Evar_defined c -> Evar_defined (f c)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 94ade8c3c..b85c67210 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
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 5e9bb653c..646316898 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -261,13 +261,18 @@ type atac = auto_result tac
 
 let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
   let cty = Evarutil.nf_evar sigma cty in
-  let keep = not only_classes || 
-    let ctx, ar = decompose_prod cty in
+  let rec iscl env ty = 
+    let ctx, ar = decompose_prod_assum ty in
       match kind_of_term (fst (decompose_app ar)) with
       | Const c -> is_class (ConstRef c)
       | Ind i -> is_class (IndRef i)
-      | _ -> false
+      | _ -> 
+	  let env' = Environ.push_rel_context ctx env in
+	  let ty' = whd_betadeltaiota env' ar in
+	       if not (eq_constr ty' ar) then iscl env' ty'
+	       else false
   in
+  let keep = not only_classes || iscl env cty in
     if keep then let c = mkVar id in
       map_succeed 
 	(fun f -> try f (c,cty) with UserError _ -> failwith "") 
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 75aa5eb7c..e692876da 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -258,7 +258,7 @@ Ltac bang :=
   match goal with
     | |- ?x =>
       match x with
-        | context [False_rect _ ?p] => elim p
+        | appcontext [False_rect _ ?p] => elim p
       end
   end.