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

7 files changed, 52 insertions, 32 deletions

diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index cc174ebace..f4ea232152 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -200,7 +200,7 @@ let declare_class_instance gr ctx params =
   try
   let cst = Declare.declare_constant ident
     (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in
-  Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true cst);
+  Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true (ConstRef cst));
   new_instance_message ident typ def
   with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str"  "++Cerrors.explain_exn e)
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index c5b54df335..7fdd6bd7e4 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -34,26 +34,36 @@ open Entries
 
 let typeclasses_db = "typeclass_instances"
 
+let set_typeclass_transparency c b = 
+  Auto.add_hints false [typeclasses_db] 
+    (Auto.HintsTransparencyEntry ([c], b))
+    
 let _ =
   Typeclasses.register_add_instance_hint
     (fun inst pri ->
       Flags.silently (fun () ->
 	Auto.add_hints false [typeclasses_db]
 	  (Auto.HintsResolveEntry
-	      [pri, false, mkConst inst])) ())
-
-let declare_instance_cst glob con =
-  let instance = Typeops.type_of_constant (Global.env ()) con in
+	      [pri, false, constr_of_global inst])) ());
+  Typeclasses.register_set_typeclass_transparency set_typeclass_transparency
+    
+let declare_class glob idl =
+  match global (Ident idl) with
+  | ConstRef x -> Typeclasses.add_constant_class x
+  | IndRef x -> Typeclasses.add_inductive_class x
+  | _ -> user_err_loc (fst idl, "declare_class", 
+		      Pp.str"Unsupported class type, only constants and inductives are allowed")
+    
+let declare_instance_cst glob c =
+  let instance = Typing.type_of (Global.env ()) Evd.empty (constr_of_global c) in
   let _, r = decompose_prod_assum instance in
     match class_of_constr r with
-      | Some tc -> add_instance (new_instance tc None glob con)
+      | Some tc -> add_instance (new_instance tc None glob c)
       | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.")
 
 let declare_instance glob idl =
-  let con =
-    try (match global (Ident idl) with
-      | ConstRef x -> x
-      | _ -> raise Not_found)
+  let con = 
+    try global (Ident idl)
     with _ -> error "Instance definition not found."
   in declare_instance_cst glob con
 
@@ -104,7 +114,7 @@ let ($$) g f = fun x -> g (f x)
 
 let instance_hook k pri global imps ?hook cst =
   let inst = Typeclasses.new_instance k pri global cst in
-    Impargs.maybe_declare_manual_implicits false (ConstRef cst) ~enriching:false imps;
+    Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
     Typeclasses.add_instance inst;
     (match hook with Some h -> h cst | None -> ())
 
@@ -120,11 +130,11 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
   in
   let kn = Declare.declare_constant id cdecl in
     Flags.if_verbose Command.definition_message id;
-    instance_hook k pri global imps ?hook kn;
+    instance_hook k pri global imps ?hook (ConstRef kn);
     id
 
 let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
-    ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri =
+    ?(tac:Proof_type.tactic option) ?(hook:(global_reference -> unit) option) pri =
   let env = Global.env() in
   let evars = ref Evd.empty in
   let tclass, ids =
@@ -177,7 +187,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 	Evarutil.check_evars env Evd.empty !evars termtype;
 	let cst = Declare.declare_internal_constant id
 	  (Entries.ParameterEntry (termtype,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
-	in instance_hook k None false imps ?hook cst; id
+	in instance_hook k None false imps ?hook (ConstRef cst); id
       end
     else
       begin
@@ -238,10 +248,10 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 	    evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars;
 	    let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	      Flags.silently (fun () ->
-		Command.start_proof id kind termtype
-		  (fun _ -> function ConstRef cst -> instance_hook k pri global imps ?hook cst
-		    | _ -> assert false);
-		if props <> [] then Pfedit.by (!refine_ref (evm, term))
+		Command.start_proof id kind termtype (fun _ -> instance_hook k pri global imps ?hook);
+		if props <> [] then 
+		  Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS ( !isevars)) *)
+		    (!refine_ref (evm, term))
 		else if Flags.is_auto_intros () then
 		  Pfedit.by (Refiner.tclDO len Tactics.intro);
 		(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
@@ -249,7 +259,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 	      id
 	  end
       end
-
+	
 let named_of_rel_context l =
   let acc, ctx =
     List.fold_right
@@ -285,7 +295,7 @@ let context ?(hook=fun _ -> ()) l =
 	in
 	  match class_of_constr t with
 	    | Some tc ->
-		add_instance (Typeclasses.new_instance tc None false cst);
+		add_instance (Typeclasses.new_instance tc None false (ConstRef cst));
 		hook (ConstRef cst)
 	    | None -> ()
       else (
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 7a8e9a9235..5953c14f94 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -29,6 +29,10 @@ val mismatched_params : env -> constr_expr list -> rel_context -> 'a
 
 val mismatched_props : env -> constr_expr list -> rel_context -> 'a
 
+(* Post-hoc class declaration. *)
+
+val declare_class : bool -> identifier located -> unit
+
 (* Instance declaration *)
 
 val declare_instance : bool -> identifier located -> unit
@@ -38,7 +42,7 @@ val declare_instance_constant :
   int option -> (* priority *)
   bool -> (* globality *)
   Impargs.manual_explicitation list -> (* implicits *)
-  ?hook:(Names.constant -> unit) ->
+  ?hook:(Libnames.global_reference -> unit) ->
   identifier -> (* name *)
   Term.constr -> (* body *)
   Term.types -> (* type *)
@@ -51,10 +55,14 @@ val new_instance :
   constr_expr ->
   ?generalize:bool ->
   ?tac:Proof_type.tactic  ->
-  ?hook:(constant -> unit) ->
+  ?hook:(Libnames.global_reference -> unit) ->
   int option ->
   identifier
 
+(* Setting opacity *)
+
+val set_typeclass_transparency : evaluable_global_reference -> bool -> unit
+
 (* For generation on names based on classes only *)
 
 val id_of_class : typeclass -> identifier
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 152ae5b706..e11a3b3736 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -287,20 +287,14 @@ let implicits_of_context ctx =
     in ExplByPos (i, explname), (true, true, true))
     1 (List.rev (Anonymous :: (List.map pi1 ctx)))
 
-let typeclasses_db = "typeclass_instances"
-
-let qualid_of_con c =
+let qualid_of_con c = 
   Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c))
 
-let set_rigid c =
-  Auto.add_hints false [typeclasses_db]
-    (Auto.HintsTransparencyEntry ([EvalConstRef c], false))
-
 let declare_instance_cst glob con =
   let instance = Typeops.type_of_constant (Global.env ()) con in
   let _, r = decompose_prod_assum instance in
     match class_of_constr r with
-      | Some tc -> add_instance (new_instance tc None glob con)
+      | Some tc -> add_instance (new_instance tc None glob (ConstRef con))
       | None -> errorlabstrm "" (Pp.strbrk "Constant does not build instances of a declared type class.")
 
 let declare_class finite def infer id idbuild paramimpls params arity fieldimpls fields
@@ -340,7 +334,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	let cref = ConstRef cst in
 	Impargs.declare_manual_implicits false cref paramimpls;
 	Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
-	set_rigid cst; (* set_rigid proj_cst; *)
+	Classes.set_typeclass_transparency (EvalConstRef cst) false;
 	if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign ();
 	cref, [proj_name, Some proj_cst]
     | _ ->
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 13b27d5abc..1d20106a5a 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -8,9 +8,9 @@ Libtypes
 Search
 Autoinstance
 Command
+Classes
 Record
 Ppvernac
-Classes
 Vernacinterp
 Mltop
 Vernacentries
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 70feb6ceb7..d2a9153fe4 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -620,6 +620,10 @@ let vernac_declare_instance id =
   Dumpglob.dump_definition id false "inst";
   Classes.declare_instance false id
 
+let vernac_declare_class id =
+  Dumpglob.dump_definition id false "class";
+  Classes.declare_class false id
+
 (***********)
 (* Solving *)
 let vernac_solve n tcom b =
@@ -1338,6 +1342,7 @@ let interp c = match c with
   | VernacInstance (glob, sup, inst, props, pri) -> vernac_instance glob sup inst props pri
   | VernacContext sup -> vernac_context sup
   | VernacDeclareInstance id -> vernac_declare_instance id
+  | VernacDeclareClass id -> vernac_declare_class id
 
   (* Solving *)
   | VernacSolve (n,tac,b) -> vernac_solve n tac b
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 2e73767c58..9bcdd402d3 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -251,6 +251,9 @@ type vernac_expr =
   | VernacDeclareInstance of
       lident (* instance name *)
 
+  | VernacDeclareClass of
+      lident (* inductive or definition name *)
+
   (* Modules and Module Types *)
   | VernacDeclareModule of bool option * lident *
       module_binder list * (module_type_ast * bool)