- 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

6 files changed, 60 insertions, 17 deletions

diff --git a/CHANGES b/CHANGES
index 1303bc4b5e..7dc51705ad 100644
--- a/CHANGES
+++ b/CHANGES
@@ -188,8 +188,9 @@ Program
   iff they can be automatically solved by the default tactic.
 - New command "Preterm [ of id ]" to see the actual term fed to Coq for
   debugging purposes.
-- New option "Transparent Obligations" to force the declaration of 
-  all obligations as transparent.
+- New option "Transparent Obligations" to control the declaration of 
+  obligations as transparent or opaque. All obligations are now transparent 
+  by default, otherwise the system declares them opaque if possible.
 - Changed the notations "left" and "right" to "in_left" and "in_right" to hide 
   the proofs in standard disjunctions, to avoid breaking existing scripts when 
   importing Program. Also, put them in program_scope.
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
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 5fe218fa50..0f6a5cbf6c 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -230,8 +230,8 @@ tactic is replaced by the default one if not specified.
   Shows the term that will be fed to
   the kernel once the obligations are solved. Useful for debugging.
 \item {\tt Set Transparent Obligations}\comindex{Set Transparent Obligations}
-  Force all obligations to be declared as transparent, otherwise let the
-  system infer which obligations can be declared opaque.
+  Control whether all obligations should be declared as transparent (the
+  default), or if the system should infer which obligations can be declared opaque. 
 \end{itemize}
 
 The module {\tt Coq.Program.Tactics} defines the default tactic for solving
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 774e03c2cc..6aadb9bbfc 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -41,6 +41,7 @@ open Libnames
 open Evd
 
 let default_eauto_depth = 100
+let typeclasses_db = "typeclass_instances"
 
 let check_imported_library d =
   let d' = List.map id_of_string d in
@@ -356,6 +357,11 @@ let full_eauto debug n lems gls =
   let db_list = List.map searchtable_map dbnames in
     e_search_auto debug n lems db_list gls
 
+let typeclasses_eauto debug n lems gls = 
+  let dbnames = [typeclasses_db] in
+  let db_list = List.map searchtable_map dbnames in
+    e_search_auto debug n lems db_list gls
+
 exception Found of evar_map
 
 let valid goals p res_sigma l = 
@@ -383,7 +389,7 @@ let resolve_all_evars_once debug (mode, depth) env p evd =
   let goals = List.rev goals in
   let gls = { it = List.map snd goals; sigma = evm' } in
   let res_sigma = ref evm' in
-  let gls', valid' = full_eauto debug (mode, depth) [] (gls, valid goals p res_sigma) in
+  let gls', valid' = typeclasses_eauto debug (mode, depth) [] (gls, valid goals p res_sigma) in
     res_sigma := Evarutil.nf_evars (sig_sig gls');
     try ignore(valid' []); assert(false) 
     with Found evm' -> Evarutil.nf_evar_defs (Evd.evars_reset_evd evm' evd)
@@ -393,7 +399,7 @@ exception FoundTerm of constr
 let resolve_one_typeclass env gl =
   let gls = { it = [ Evd.make_evar (Environ.named_context_val env) gl ] ; sigma = Evd.empty } in
   let valid x = raise (FoundTerm (fst (Refiner.extract_open_proof Evd.empty (List.hd x)))) in
-  let gls', valid' = full_eauto false (true, default_eauto_depth) [] (gls, valid) in
+  let gls', valid' = typeclasses_eauto false (true, default_eauto_depth) [] (gls, valid) in
     try ignore(valid' []); assert false with FoundTerm t -> 
       let term = Evarutil.nf_evar (sig_sig gls') t in
 	if occur_existential term then raise Not_found else term
@@ -417,7 +423,7 @@ let resolve_all_evars debug m env p oevd =
     
 VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings
 | [ "Typeclasses" "unfold" reference_list(cl) ] -> [
-    add_hints false ["typeclass_instances"] (Vernacexpr.HintsUnfold cl)
+    add_hints false [typeclasses_db] (Vernacexpr.HintsUnfold cl)
   ]
 END
 
@@ -1512,3 +1518,27 @@ END
 TACTIC EXTEND setoid_transitivity
    [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ]
 END
+
+let try_classes t gls = 
+  try t gls
+  with (Pretype_errors.PretypeError _) as e -> raise e
+
+TACTIC EXTEND try_classes
+  [ "try_classes" tactic(t) ] -> [ try_classes (snd t) ]
+END
+
+(* let lift_monad env t = *)
+(*   match kind_of_term t with *)
+(*     | Rel n -> t *)
+(*     | Var id -> t *)
+(*     | App (f, args) -> *)
+(* 	let args' =  *)
+(* 	  List.fold_right *)
+(* 	    (fun arg acc -> *)
+(* 	      let ty = Typing.type_of env arg in *)
+(* 	      let arg' = lift_monad t in *)
+(* 		monad_bind arg'  *)
+(* 		  (mkLambda (Name (id_of_string "x"),  *)
+			    
+			    
+			    
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