diff options
| author | Maxime Dénès | 2018-11-20 08:42:52 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-20 08:42:52 +0100 |
| commit | 4d26550af26c1dab464253cc470e8a876fee0025 (patch) | |
| tree | f2594e7e0b7960c50d45d6cb2e782eb074d19150 /tactics/equality.ml | |
| parent | 22c0b10f139d9a30fcbe4a5a489022e2b94130e9 (diff) | |
| parent | 4acdbe9be526dc7f646ab084e52fe4b9a6ad1399 (diff) | |
Merge PR #7925: Clean transparent state
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index c4a6b1605d..969f539d1f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -101,8 +101,8 @@ 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; + modulo_delta = TransparentState.empty; + modulo_delta_types = TransparentState.empty; check_applied_meta_types = true; use_pattern_unification = true; use_meta_bound_pattern_unification = true; @@ -169,7 +169,7 @@ let instantiate_lemma gl c ty l l2r concl = [eqclause] let rewrite_conv_closed_core_unif_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; + modulo_conv_on_closed_terms = Some TransparentState.full; (* We have this flag for historical reasons, it has e.g. the consequence *) (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *) @@ -178,8 +178,8 @@ let rewrite_conv_closed_core_unif_flags = { (* 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" *) - modulo_delta = empty_transparent_state; - modulo_delta_types = full_transparent_state; + modulo_delta = TransparentState.empty; + modulo_delta_types = TransparentState.full; check_applied_meta_types = true; use_pattern_unification = true; (* To rewrite "?n x y" in "y+x=0" when ?n is *) @@ -204,7 +204,7 @@ let rewrite_conv_closed_unif_flags = { } let rewrite_keyed_core_unif_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; + modulo_conv_on_closed_terms = Some TransparentState.full; (* We have this flag for historical reasons, it has e.g. the consequence *) (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *) @@ -213,8 +213,8 @@ let rewrite_keyed_core_unif_flags = { (* 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" *) - modulo_delta = full_transparent_state; - modulo_delta_types = full_transparent_state; + modulo_delta = TransparentState.full; + modulo_delta_types = TransparentState.full; check_applied_meta_types = true; use_pattern_unification = true; (* To rewrite "?n x y" in "y+x=0" when ?n is *) |