- Fix bug related to indices of fixpoints.

- Add a typeclasses_eauto which uses only the typeclass_instances
  database.
- Set obligations as transparent by default to avoid the 
  common problem with ill-formed recursive defs due to opaque
  obligations.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10925 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 4 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7d2a437766..8905907a15 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -791,8 +791,15 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let names = List.map (fun id -> Name id) fixnames in
   (Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
 
+(* Jump over let-bindings. *)
+
 let rel_index n ctx = 
-  list_index0 (Name n) (List.rev_map (fun (na, _, _) -> na) ctx)
+  list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx))
+
+let rec unfold f b =
+  match f b with
+    | Some (x, b') -> x :: unfold f b'
+    | None -> []
 
 let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
   match n with 
@@ -803,9 +810,9 @@ let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
 	 but doing it properly involves delta-reduction, and it finally 
          doesn't seem to worth the effort (except for huge mutual 
 	 fixpoints ?) *)
-      let m = List.length fixctx in
-      let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
-      list_map_i (fun i _ -> i) 0 ctx
+      let len = List.length fixctx in
+	unfold (function x when x = len -> None 
+	  | n -> Some (n, succ n)) 0
 
 let interp_recursive fixkind l boxed =
   let env = Global.env() in