diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 6 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index ac3f52c6ef..c7703b52c7 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -101,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 TranspState.full; + 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 = TranspState.empty; - modulo_delta_types = TranspState.full; + 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 fb42a9cebe..6c4193c66b 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -37,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 TranspState.full 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 1aaf762e31..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) TranspState.empty 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 |