Integrate a few improvements on typeclasses and Program from the equations branch

and remove equations stuff which moves to a separate plugin.

Classes:
- Ability to define classes post-hoc from constants or inductive types.
- Correctly rebuild the hint database associated to local hypotheses when 
  they are changed by a [Hint Extern] in typeclass resolution.

Tactics and proofs:
- Change [revert] so that it keeps let-ins (but not [generalize]).
- Various improvements to the [generalize_eqs] tactic to make it more robust
  and produce the smallest proof terms possible.
  Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with 
  [generalize_eqs].
- A few new general purpose tactics in Program.Tactics like [revert_until]
- Make transitive closure well-foundedness proofs transparent.
- More uniform testing for metas/evars in pretyping/unification.ml
  (might introduce a few changes in the contribs).

Program:
- Better sorting of dependencies in obligations.
- Ability to start a Program definition from just a type and no obligations, 
  automatically adding an obligation for this type.
- In compilation of Program's well-founded definitions, make the functional a
  separate definition for easier reasoning.
- Add a hint database for every Program populated by [Hint Unfold]s for 
  every defined obligation constant.


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

1 files changed, 23 insertions, 15 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index dd11e1ef0e..5de89baa64 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -123,6 +123,7 @@ module Hint_db = struct
 
   type t = {
     hintdb_state : Names.transparent_state;
+    hintdb_unfolds : Idset.t * Cset.t;
     use_dn : bool;
     hintdb_map : search_entry Constr_map.t;
     (* A list of unindexed entries starting with an unfoldable constant
@@ -131,6 +132,7 @@ module Hint_db = struct
   }
 
   let empty st use_dn = { hintdb_state = st;
+			  hintdb_unfolds = (Idset.empty, Cset.empty);
 			  use_dn = use_dn;
 			  hintdb_map = Constr_map.empty;
 			  hintdb_nopat = [] }
@@ -179,14 +181,17 @@ module Hint_db = struct
       List.fold_left (fun db (gr,v) -> addkv gr v db) db' db.hintdb_nopat
 
   let add_one (k,v) db =
-    let st',rebuild =
+    let st',db,rebuild =
       match v.code with
       | Unfold_nth egr ->
-	  let (ids,csts) = db.hintdb_state in
-	    (match egr with
-	    | EvalVarRef id -> (Idpred.add id ids, csts)
-	    | EvalConstRef cst -> (ids, Cpred.add cst csts)), true
-      | _ -> db.hintdb_state, false
+	  let addunf (ids,csts) (ids',csts') =
+	    match egr with
+	    | EvalVarRef id -> (Idpred.add id ids, csts), (Idset.add id ids', csts')
+	    | EvalConstRef cst -> (ids, Cpred.add cst csts), (ids', Cset.add cst csts')
+	  in 
+	  let state, unfs = addunf db.hintdb_state db.hintdb_unfolds in
+	    state, { db with hintdb_unfolds = unfs }, true
+      | _ -> db.hintdb_state, db, false
     in
     let db = if db.use_dn && rebuild then rebuild_db st' db else db
     in addkv k v db
@@ -203,6 +208,8 @@ module Hint_db = struct
     if db.use_dn then rebuild_db st db
     else { db with hintdb_state = st }
 
+  let unfolds db = db.hintdb_unfolds
+
   let use_dn db = db.use_dn
 
 end
@@ -356,17 +363,18 @@ open Vernacexpr
 
 (* If the database does not exist, it is created *)
 (* TODO: should a warning be printed in this case ?? *)
-let add_hint dbname hintlist =
-  try
-    let db = searchtable_map dbname in
-    let db' = Hint_db.add_list hintlist db in
+
+let get_db dbname =
+  try searchtable_map dbname
+  with Not_found -> Hint_db.empty empty_transparent_state false
+
+let add_hint dbname hintlist = 
+  let db = get_db dbname in
+  let db' = Hint_db.add_list hintlist db in
     searchtable_add (dbname,db')
-  with Not_found ->
-    let db = Hint_db.add_list hintlist (Hint_db.empty empty_transparent_state false) in
-    searchtable_add (dbname,db)
 
 let add_transparency dbname grs b =
-  let db = searchtable_map dbname in
+  let db = get_db dbname in
   let st = Hint_db.transparent_state db in
   let st' =
     List.fold_left (fun (ids, csts) gr ->
@@ -882,7 +890,7 @@ and tac_of_hint db_list local_db concl (flags, {pat=p; code=t}) =
       tclTHEN
         (unify_resolve_gen flags (term,cl))
         (trivial_fail_db (flags <> None) db_list local_db)
-  | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
+  | Unfold_nth c -> tclPROGRESS (unfold_in_concl [all_occurrences,c])
   | Extern tacast -> conclPattern concl p tacast
 
 and trivial_resolve mod_delta db_list local_db cl =