diff options
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 |