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, 5 insertions, 6 deletions

diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 0884b3462..07de95d8e 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -201,8 +201,8 @@ let build_signature evars env m (cstrs : 'a option list) (finalcstr : 'a option)
 	      if obj = None then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
 	      else error "build_signature: no constraint can apply on a dependent argument"
 	  else
-	    let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
 	    let ty = Reductionops.nf_betaiota (fst evars) ty in
+	    let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
 	    let evars, relty = mk_relty evars env ty obj in
 	    let newarg = mkApp (Lazy.force respectful, [| ty ; b' ; relty ; arg |]) in
 	      evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs
@@ -1279,8 +1279,8 @@ let add_morphism_infer glob m n =
       let cst = Declare.declare_internal_constant instance_id
 				(Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
-				add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob cst);
-				declare_projection n instance_id (ConstRef cst)
+	add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst));
+	declare_projection n instance_id (ConstRef cst)
     else
       let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	Flags.silently
@@ -1289,7 +1289,7 @@ let add_morphism_infer glob m n =
 	      (fun _ -> function
 		Libnames.ConstRef cst ->
 		  add_instance (Typeclasses.new_instance (Lazy.force proper_class) None
-				   glob cst);
+				   glob (ConstRef cst));
 		  declare_projection n instance_id (ConstRef cst)
 		| _ -> assert false);
 	    Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) ();
@@ -1306,8 +1306,7 @@ let add_morphism glob binders m s n =
   in
   let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
     ignore(new_instance ~global:glob binders instance (CRecord (dummy_loc,None,[]))
-	      ~generalize:false ~tac
-	      ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst)) None)
+	      ~generalize:false ~tac ~hook:(declare_projection n instance_id) None)
 
 VERNAC COMMAND EXTEND AddSetoid1
    [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->