diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-08-23 12:37:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-08 20:46:08 +0200 |
| commit | a9f8fa56e76aa557b1391cb9709cb893a4f602ce (patch) | |
| tree | 9ef357486083ebefa0a9b2ef328270b74f5dad93 /pretyping/reductionops.ml | |
| parent | b1fbec7e3945fe2965f4ba9f80c8c31b821dbce1 (diff) | |
Using EConstr equality check in unification.
The code from Universes what essentially a duplicate of the one from EConstr,
but they were copied for historical reasons. Now, this is not useful anymore,
so that we remove the implementation from Universes and rely on the one from
EConstr.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 356323543..2aa2f9013 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1438,17 +1438,13 @@ let sigma_univ_state = let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = (** FIXME *) - let open Universes in - let x = EConstr.Unsafe.to_constr x in - let y = EConstr.Unsafe.to_constr y in try - let fold cstr accu = Some (Constraints.fold Constraints.add cstr accu) in let b, sigma = let ans = if pb == Reduction.CUMUL then - Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty + EConstr.leq_constr_universes sigma x y else - Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty + EConstr.eq_constr_universes sigma x y in let ans = match ans with | None -> None @@ -1462,6 +1458,8 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) in if b then sigma, true else + let x = EConstr.Unsafe.to_constr x in + let y = EConstr.Unsafe.to_constr y in let sigma' = conv_fun pb ~l2r:false sigma ts env (sigma, sigma_univ_state) x y in |