- 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

2 files changed, 11 insertions, 6 deletions

diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index da0e4a8e56..3b4067ce89 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -334,20 +334,25 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
   (Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
 
 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 
-  | Some (loc, n) -> [rel_index n fixctx] 
+  | Some (loc, n) -> [rel_index n fixctx]
   | None -> 
       (* If recursive argument was not given by user, we try all args.
 	 An earlier approach was to look only for inductive arguments,
 	 but doing it properly involves delta-reduction, and it finally 
          doesn't seem to worth the effort (except for huge mutual 
 	 fixpoints ?) *)
-      let m = Term.nb_prod fixtype 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 push_named_context = List.fold_right push_named
 
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index bc6d5dee1a..1e6a55a0e7 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -61,7 +61,7 @@ let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ())
 let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t
 
 (* true = All transparent, false = Opaque if possible *)
-let proofs_transparency = ref false
+let proofs_transparency = ref true
 
 let set_proofs_transparency = (:=) proofs_transparency
 let get_proofs_transparency () = !proofs_transparency