diff options
| -rw-r--r-- | pretyping/unification.ml | 14 | ||||
| -rw-r--r-- | pretyping/unification.mli | 1 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 1 | ||||
| -rw-r--r-- | tactics/auto.ml | 1 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 1 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 1 |
8 files changed, 21 insertions, 3 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 82a02d909..1193359cb 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -202,6 +202,10 @@ type unify_flags = { modulo_delta_types : Names.transparent_state; + check_applied_meta_types : bool; + (* This controls whether meta's applied to arguments have their *) + (* type unified with the type of their instance *) + resolve_evars : bool; (* This says if type classes instances resolution must be used to infer *) (* the remaining evars *) @@ -241,6 +245,7 @@ let default_unify_flags = { use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = full_transparent_state; modulo_delta_types = full_transparent_state; + check_applied_meta_types = true; resolve_evars = false; use_pattern_unification = true; use_meta_bound_pattern_unification = true; @@ -261,6 +266,7 @@ let default_no_delta_unify_flags = { use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; + check_applied_meta_types = false; resolve_evars = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; @@ -281,6 +287,7 @@ let elim_flags = { use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = full_transparent_state; modulo_delta_types = full_transparent_state; + check_applied_meta_types = true; resolve_evars = false; use_pattern_unification = true; use_meta_bound_pattern_unification = true; @@ -296,6 +303,7 @@ let elim_no_delta_flags = { use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; + check_applied_meta_types = false; resolve_evars = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; @@ -371,7 +379,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag if k1 = k2 then substn else let stM,stN = extract_instance_status pb in let (sigma,metasubst,evarsubst) = - if wt then + if wt && flags.check_applied_meta_types then let tyM = subst_metas metasubst (Typing.meta_type sigma k1) in let tyN = subst_metas metasubst (Typing.meta_type sigma k2) in unirec_rec curenvnb CONV true false substn tyM tyN @@ -381,7 +389,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag else sigma,(k2,cM,stM)::metasubst,evarsubst | Meta k, _ when not (dependent cM cN) -> let (sigma,metasubst,evarsubst) = - if wt then + if wt && flags.check_applied_meta_types then let tyM = subst_metas metasubst (Typing.meta_type sigma k) in let tyN = subst_metas metasubst (get_type_of curenv sigma cN) in unirec_rec curenvnb CONV true false substn tyM tyN @@ -397,7 +405,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag else error_cannot_unify_local curenv sigma (m,n,cN) | _, Meta k when not (dependent cN cM) -> let (sigma,metasubst,evarsubst) = - if wt then + if wt && flags.check_applied_meta_types then let tyM = subst_metas metasubst (get_type_of curenv sigma cM) in let tyN = subst_metas metasubst (Typing.meta_type sigma k) in unirec_rec curenvnb CONV true false substn tyM tyN diff --git a/pretyping/unification.mli b/pretyping/unification.mli index d28451177..e4bca4d33 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -15,6 +15,7 @@ type unify_flags = { use_metas_eagerly_in_conv_on_closed_terms : bool; modulo_delta : Names.transparent_state; modulo_delta_types : Names.transparent_state; + check_applied_meta_types : bool; resolve_evars : bool; use_pattern_unification : bool; use_meta_bound_pattern_unification : bool; diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index ff84a343b..eb935d05d 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -105,6 +105,7 @@ let fail_quick_unif_flags = { use_metas_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; + check_applied_meta_types = false; resolve_evars = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; (* ? *) diff --git a/tactics/auto.ml b/tactics/auto.ml index e15c30a3b..93ca89f47 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1021,6 +1021,7 @@ let auto_unif_flags = { use_metas_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; + check_applied_meta_types = false; resolve_evars = true; use_pattern_unification = false; use_meta_bound_pattern_unification = true; diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index e219bbff0..42df244de 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -77,6 +77,7 @@ let auto_unif_flags = { use_metas_eagerly_in_conv_on_closed_terms = true; modulo_delta = var_full_transparent_state; modulo_delta_types = full_transparent_state; + check_applied_meta_types = false; resolve_evars = false; use_pattern_unification = true; use_meta_bound_pattern_unification = true; diff --git a/tactics/equality.ml b/tactics/equality.ml index 76bceb738..10fd0fef9 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -87,6 +87,7 @@ let rewrite_unif_flags = { Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = empty_transparent_state; + Unification.check_applied_meta_types = true; Unification.resolve_evars = true; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; @@ -154,6 +155,7 @@ let rewrite_conv_closed_unif_flags = { Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = full_transparent_state; + Unification.check_applied_meta_types = true; Unification.resolve_evars = false; Unification.use_pattern_unification = true; (* To rewrite "?n x y" in "y+x=0" when ?n is *) diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 80930af42..d297969d1 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -299,6 +299,7 @@ let rewrite_unif_flags = { Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = full_transparent_state; + Unification.check_applied_meta_types = true; Unification.resolve_evars = true; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; @@ -314,6 +315,7 @@ let rewrite2_unif_flags = Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = conv_transparent_state; + Unification.check_applied_meta_types = true; Unification.resolve_evars = true; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; @@ -330,6 +332,7 @@ let general_rewrite_unif_flags () = Unification.use_metas_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = ts; Unification.modulo_delta_types = ts; + Unification.check_applied_meta_types = true; Unification.resolve_evars = true; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 1b35888c0..988d9f530 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1690,6 +1690,7 @@ let default_matching_flags sigma = { use_metas_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; + check_applied_meta_types = true; resolve_evars = false; use_pattern_unification = false; use_meta_bound_pattern_unification = false; |