Little fixes in setoid_rewrite.

- More meaningful argument name for resolve_typeclasses. 
- Try to remove unneeded instance declarations in
Morphisms. 
- Allow the proofs of reflexivity arising from unchanged
arguments in setoid_rewrite to be fullfiled by Morphism instances and
not necessariy because the relation is reflexive (needed by
higher-order morphisms). Use a new "MorphismProxy" class to implement
that efficiently.
- Fix a bug in abstract_generalize not delta-reducing a type where it should.


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

3 files changed, 3 insertions, 3 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 7ec5d3575f..4a848380ef 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -158,7 +158,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
   let env' = Classes.push_named_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
   let sigma = Evd.evars_of !isevars in
-  isevars := resolve_typeclasses ~onlyargs:false ~all:true env' sigma !isevars;
+  isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' sigma !isevars;
   let sigma = Evd.evars_of !isevars in
   let substctx = Typeclasses.nf_substitution sigma subst in
   let subst, _propsctx = 
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index b9bda64a9a..ec5af37fe2 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -73,7 +73,7 @@ let interp env isevars c tycon =
   let _ = isevars := Evarutil.nf_evar_defs !isevars in
   let evd,_ = consider_remaining_unif_problems env !isevars in
 (*   let unevd = undefined_evars evd in *)
-  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (Evd.evars_of evd) evd in
+  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env (Evd.evars_of evd) evd in
   let evm = evars_of unevd' in
     isevars := unevd';
     nf_evar evm j.uj_val, nf_evar evm j.uj_type
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index d3edb6e3cd..e87eb27dca 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -558,7 +558,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
       | IsType ->
 	  (pretype_type empty_valcon env isevars lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !isevars in
-    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (evars_of evd) evd in
+    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env (evars_of evd) evd in
       isevars:=evd;
       nf_evar (evars_of !isevars) c'