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

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index df1e45d86..19df941b2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -653,7 +653,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       | IsType ->
 	  (pretype_type empty_valcon env evdref lvar c).utj_val in
     let evd,_ = consider_remaining_unif_problems env !evdref 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
       evdref := evd;
       nf_evar (evars_of evd) c'
 
@@ -667,7 +667,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let j = pretype empty_tycon env evdref ([],[]) c in
     let evd,_ = consider_remaining_unif_problems env !evdref in
     let j = j_nf_evar (evars_of evd) j in
-    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:true env (evars_of evd) evd in
+    let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env (evars_of evd) evd in
     let j = j_nf_evar (evars_of evd) j in
     check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
     j
@@ -687,7 +687,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let c = pretype_gen evdref env lvar kind c in
     let evd,_ = consider_remaining_unif_problems env !evdref in
       if fail_evar then 
-	let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~all:false env (evars_of evd) evd in
+	let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env (evars_of evd) evd in
 	let c = Evarutil.nf_isevar evd c in
 	  check_evars env Evd.empty evd c;
 	  evd, c
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 045070960..e9a766a92 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -407,10 +407,10 @@ let has_typeclasses evd =
 	&& is_resolvable evi))
     evd false
 
-let resolve_typeclasses ?(onlyargs=false) ?(all=true) env sigma evd =
+let resolve_typeclasses ?(onlyargs=false) ?(fail=true) env sigma evd =
   if not (has_typeclasses sigma) then evd
   else
-    !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs all
+    !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs fail
 
 type substitution = (identifier * constr) list
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index d35ee5414..c6763a421 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -74,7 +74,7 @@ val bool_out : Dyn.t -> bool
 val is_resolvable : evar_info -> bool
 val mark_unresolvable : evar_info -> evar_info
 
-val resolve_typeclasses : ?onlyargs:bool -> ?all:bool -> env -> evar_map -> evar_defs -> evar_defs
+val resolve_typeclasses : ?onlyargs:bool -> ?fail:bool -> env -> evar_map -> evar_defs -> evar_defs
 
 val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref
 val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> evar_defs) ref