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 /proofs | |
| parent | 22c0b10f139d9a30fcbe4a5a489022e2b94130e9 (diff) | |
| parent | 4acdbe9be526dc7f646ab084e52fe4b9a6ad1399 (diff) | |
Merge PR #7925: Clean transparent state
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 7 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 3 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 2 |
3 files changed, 5 insertions, 7 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index b99cf245fe..c7703b52c7 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -9,7 +9,6 @@ (************************************************************************) open Util -open Names open Constr open Termops open Evd @@ -102,11 +101,11 @@ let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv = provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) let fail_quick_core_unif_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; + modulo_conv_on_closed_terms = Some TransparentState.full; 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; + modulo_delta = TransparentState.empty; + modulo_delta_types = TransparentState.full; check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; (* ? *) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index cb71f09826..6c4193c66b 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -10,7 +10,6 @@ open CErrors open Util -open Names open Evd open Evarutil open Evarsolve @@ -38,7 +37,7 @@ let define_and_solve_constraints evk c env evd = match List.fold_left (fun p (pbty,env,t1,t2) -> match p with - | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2 + | Success evd -> Evarconv.evar_conv_x TransparentState.full env evd pbty t1 t2 | UnifFailure _ as x -> x) (Success evd) pbs with diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 56ce744bc1..0981584bb5 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -160,7 +160,7 @@ let make_flag env f = (fun v red -> red_sub red (make_flag_constant v)) f.rConst red else (* Only rConst *) - let red = red_add_transparent (red_add red fDELTA) all_opaque in + let red = red_add_transparent (red_add red fDELTA) TransparentState.empty in List.fold_right (fun v red -> red_add red (make_flag_constant v)) f.rConst red |