diff options
| -rw-r--r-- | pretyping/unification.ml | 10 | ||||
| -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.ml | 1 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 3 | ||||
| -rw-r--r-- | test-suite/success/setoid_unif.v | 27 |
8 files changed, 43 insertions, 3 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index a6b02bcf9..982b8a3ec 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -234,6 +234,8 @@ type core_unify_flags = { (* This refinement of the conversion on closed terms is activable *) (* (and activated for apply, rewrite but not auto since Feb 2008 for 8.2) *) + use_evars_eagerly_in_conv_on_closed_terms : bool; + modulo_delta : Names.transparent_state; (* This controls which constants are unfoldable; this is on for apply *) (* (but not simple apply) since Feb 2008 for 8.2 *) @@ -299,6 +301,7 @@ let default_core_unify_flags () = let ts = Names.full_transparent_state in { modulo_conv_on_closed_terms = Some ts; use_metas_eagerly_in_conv_on_closed_terms = true; + use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = ts; modulo_delta_types = ts; check_applied_meta_types = true; @@ -509,10 +512,10 @@ let isAllowedEvar flags c = match kind_of_term c with | _ -> false let check_compatibility env pbty flags (sigma,metasubst,evarsubst) tyM tyN = - match subst_defined_metas_evars (metasubst,evarsubst) tyM with + match subst_defined_metas_evars (metasubst,[]) tyM with | None -> sigma | Some m -> - match subst_defined_metas_evars (metasubst,evarsubst) tyN with + match subst_defined_metas_evars (metasubst,[]) tyN with | None -> sigma | Some n -> if is_ground_term sigma m && is_ground_term sigma n then @@ -844,7 +847,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb match flags.modulo_conv_on_closed_terms with | None -> None | Some convflags -> - let subst = if flags.use_metas_eagerly_in_conv_on_closed_terms then (metasubst,evarsubst) else (ms,es) in + let subst = ((if flags.use_metas_eagerly_in_conv_on_closed_terms then metasubst else ms), (if flags.use_evars_eagerly_in_conv_on_closed_terms then evarsubst else es)) in match subst_defined_metas_evars subst cM with | None -> (* some undefined Metas in cM *) None | Some m1 -> @@ -1371,6 +1374,7 @@ let default_matching_core_flags sigma = let ts = Names.full_transparent_state in { modulo_conv_on_closed_terms = Some empty_transparent_state; use_metas_eagerly_in_conv_on_closed_terms = false; + use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = ts; check_applied_meta_types = true; diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 0f5a62bb5..ce74852d3 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -13,6 +13,7 @@ open Evd type core_unify_flags = { modulo_conv_on_closed_terms : Names.transparent_state option; use_metas_eagerly_in_conv_on_closed_terms : bool; + use_evars_eagerly_in_conv_on_closed_terms : bool; modulo_delta : Names.transparent_state; modulo_delta_types : Names.transparent_state; check_applied_meta_types : bool; diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 7d25bb665..087ac0c33 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -96,6 +96,7 @@ let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv = let fail_quick_core_unif_flags = { modulo_conv_on_closed_terms = Some full_transparent_state; use_metas_eagerly_in_conv_on_closed_terms = false; + use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = full_transparent_state; check_applied_meta_types = false; diff --git a/tactics/auto.ml b/tactics/auto.ml index 18beedf95..43aa84e7a 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -43,6 +43,7 @@ open Unification let auto_core_unif_flags_of st1 st2 useeager = { modulo_conv_on_closed_terms = Some st1; use_metas_eagerly_in_conv_on_closed_terms = useeager; + use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = st2; modulo_delta_types = full_transparent_state; check_applied_meta_types = false; diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 1e6caca57..a90d1e912 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -56,6 +56,7 @@ open Unification let auto_core_unif_flags st freeze = { modulo_conv_on_closed_terms = Some st; use_metas_eagerly_in_conv_on_closed_terms = true; + use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = st; modulo_delta_types = st; check_applied_meta_types = false; diff --git a/tactics/equality.ml b/tactics/equality.ml index 425e9f290..4da80811b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -103,6 +103,7 @@ type conditions = let rewrite_core_unif_flags = { modulo_conv_on_closed_terms = None; use_metas_eagerly_in_conv_on_closed_terms = true; + use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = empty_transparent_state; modulo_delta_types = empty_transparent_state; check_applied_meta_types = true; @@ -175,6 +176,7 @@ let rewrite_conv_closed_core_unif_flags = { (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *) use_metas_eagerly_in_conv_on_closed_terms = true; + use_evars_eagerly_in_conv_on_closed_terms = false; (* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *) (* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *) diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index a96bc5e42..149dc2545 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -530,6 +530,7 @@ let rewrite_transparent_state () = let rewrite_core_unif_flags = { Unification.modulo_conv_on_closed_terms = None; Unification.use_metas_eagerly_in_conv_on_closed_terms = true; + Unification.use_evars_eagerly_in_conv_on_closed_terms = false; Unification.modulo_delta = empty_transparent_state; Unification.modulo_delta_types = full_transparent_state; Unification.check_applied_meta_types = true; @@ -552,6 +553,7 @@ let rewrite_unif_flags = { let rewrite2_unif_core_flags = { Unification.modulo_conv_on_closed_terms = Some conv_transparent_state; Unification.use_metas_eagerly_in_conv_on_closed_terms = true; + Unification.use_evars_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; @@ -576,6 +578,7 @@ let general_rewrite_unif_flags () = let core_flags = { Unification.modulo_conv_on_closed_terms = Some ts; Unification.use_metas_eagerly_in_conv_on_closed_terms = true; + Unification.use_evars_eagerly_in_conv_on_closed_terms = false; Unification.modulo_delta = ts; Unification.modulo_delta_types = ts; Unification.check_applied_meta_types = true; diff --git a/test-suite/success/setoid_unif.v b/test-suite/success/setoid_unif.v new file mode 100644 index 000000000..912596b4a --- /dev/null +++ b/test-suite/success/setoid_unif.v @@ -0,0 +1,27 @@ +(* An example of unification in rewrite which uses eager substitution + of metas (provided by Pierre-Marie). + + Put in the test suite as an indication of what the use metas + eagerly flag provides, even though the concrete cases that use it + are seldom. Today supported thanks to a new flag for using evars + eagerly, after this variant of setoid rewrite started to use clause + environments based on evars (fbbe491cfa157da627) *) + +Require Import Setoid. + +Parameter elt : Type. +Parameter T : Type -> Type. +Parameter empty : forall A, T A. +Parameter MapsTo : forall A : Type, elt -> A -> T A -> Prop. + +(* Definition In A x t := exists e, MapsTo A x e t. *) +Axiom In : forall A, A -> T A -> Prop. +Axiom foo : forall A x, In A x (empty A) <-> False. + +Record R := { t : T unit; s : unit }. +Definition Empty := {| t := empty unit; s := tt |}. + +Goal forall x, ~ In _ x (t Empty). +Proof. +intros x. +rewrite foo. |