From ec837079f89825855777a6d7c325f7163e92977c Mon Sep 17 00:00:00 2001 From: msozeau Date: Thu, 17 Apr 2008 11:54:25 +0000 Subject: 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 --- pretyping/pretyping.ml | 6 +++--- pretyping/typeclasses.ml | 4 ++-- pretyping/typeclasses.mli | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) (limited to 'pretyping') 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 -- cgit v1.2.3