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 /plugins/ltac | |
| parent | 22c0b10f139d9a30fcbe4a5a489022e2b94130e9 (diff) | |
| parent | 4acdbe9be526dc7f646ab084e52fe4b9a6ad1399 (diff) | |
Merge PR #7925: Clean transparent state
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 16cb75ea2f..fee469032c 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -528,7 +528,7 @@ let decompose_applied_relation env sigma (c,l) = let rewrite_db = "rewrite" -let conv_transparent_state = (Id.Pred.empty, Cpred.full) +let conv_transparent_state = TransparentState.cst_full let rewrite_transparent_state () = Hints.Hint_db.transparent_state (Hints.searchtable_map rewrite_db) @@ -537,8 +537,8 @@ 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 = true; - Unification.modulo_delta = empty_transparent_state; - Unification.modulo_delta_types = full_transparent_state; + Unification.modulo_delta = TransparentState.empty; + Unification.modulo_delta_types = TransparentState.full; Unification.check_applied_meta_types = true; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; @@ -585,12 +585,12 @@ let general_rewrite_unif_flags () = Unification.modulo_conv_on_closed_terms = Some ts; Unification.use_evars_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = ts; - Unification.modulo_delta_types = full_transparent_state; + Unification.modulo_delta_types = TransparentState.full; Unification.modulo_betaiota = true } in { Unification.core_unify_flags = core_flags; Unification.merge_unify_flags = core_flags; - Unification.subterm_unify_flags = { core_flags with Unification.modulo_delta = empty_transparent_state }; + Unification.subterm_unify_flags = { core_flags with Unification.modulo_delta = TransparentState.empty }; Unification.allow_K_in_toplevel_higher_order_unification = true; Unification.resolve_evars = true } |