diff options
| -rw-r--r-- | engine/evarutil.ml | 6 | ||||
| -rw-r--r-- | engine/evd.ml | 7 | ||||
| -rw-r--r-- | engine/evd.mli | 5 | ||||
| -rw-r--r-- | engine/uState.ml | 5 | ||||
| -rw-r--r-- | engine/uState.mli | 3 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 2 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 2 | ||||
| -rw-r--r-- | tactics/leminv.ml | 2 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 2 | ||||
| -rw-r--r-- | vernac/comDefinition.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
12 files changed, 25 insertions, 15 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 7674cf67a..6b3ce048f 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -89,15 +89,15 @@ let nf_evars_universes evm = (Evd.universe_subst evm) let nf_evars_and_universes evm = - let evm = Evd.nf_constraints evm in + let evm = Evd.minimize_universes evm in evm, nf_evars_universes evm let e_nf_evars_and_universes evdref = - evdref := Evd.nf_constraints !evdref; + evdref := Evd.minimize_universes !evdref; nf_evars_universes !evdref, Evd.universe_subst !evdref let nf_evar_map_universes evm = - let evm = Evd.nf_constraints evm in + let evm = Evd.minimize_universes evm in let subst = Evd.universe_subst evm in if Univ.LMap.is_empty subst then evm, nf_evar0 evm else diff --git a/engine/evd.ml b/engine/evd.ml index 47fa48d4f..185cab101 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -900,9 +900,9 @@ let nf_univ_variables evd = let evd' = {evd with universes = uctx'} in evd', subst -let nf_constraints evd = +let minimize_universes evd = let subst, uctx' = UState.normalize_variables evd.universes in - let uctx' = UState.normalize uctx' in + let uctx' = UState.minimize uctx' in {evd with universes = uctx'} let universe_of_name evd s = UState.universe_of_name evd.universes s @@ -1167,4 +1167,5 @@ let make_evar_universe_context e l = | Some l -> UState.make_with_initial_binders g l let normalize_evar_universe_context_variables = UState.normalize_variables let abstract_undefined_variables = UState.abstract_undefined_variables -let normalize_evar_universe_context = UState.normalize +let normalize_evar_universe_context = UState.minimize +let nf_constraints = minimize_universes diff --git a/engine/evd.mli b/engine/evd.mli index 25dc8c993..7957eaa01 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -533,7 +533,7 @@ val normalize_evar_universe_context_variables : UState.t -> [@@ocaml.deprecated "Alias of UState.normalize_variables"] val normalize_evar_universe_context : UState.t -> UState.t -[@@ocaml.deprecated "Alias of UState.normalize"] +[@@ocaml.deprecated "Alias of UState.minimize"] val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t @@ -598,7 +598,10 @@ val fix_undefined_variables : evar_map -> evar_map val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst +(** Universe minimization *) +val minimize_universes : evar_map -> evar_map val nf_constraints : evar_map -> evar_map +[@@ocaml.deprecated "Alias of Evd.minimize_universes"] val update_sigma_env : evar_map -> env -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index 67479351a..e57afd743 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -585,7 +585,7 @@ let refresh_undefined_univ_variables uctx = uctx_initial_universes = initial } in uctx', subst -let normalize uctx = +let minimize uctx = let ((vars',algs'), us') = Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic @@ -613,3 +613,6 @@ let update_sigma_env uctx env = uctx_universes = univs } in merge true univ_rigid eunivs eunivs.uctx_local + +(** Deprecated *) +let normalize = minimize diff --git a/engine/uState.mli b/engine/uState.mli index ef7cee32e..9a2bc706b 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -133,7 +133,10 @@ val fix_undefined_variables : t -> t val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst +(** Universe minimization *) +val minimize : t -> t val normalize : t -> t +[@@ocaml.deprecated "Alias of UState.minimize"] type universe_decl = (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 6e38b4641..e0368153e 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1922,7 +1922,7 @@ let build_morphism_signature env sigma m = in let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in let evd = solve_constraints env !evd in - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in Pretyping.check_evars env Evd.empty evd (EConstr.of_constr m); Evd.evar_universe_context evd, m diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index b290a20ff..8b5b739a3 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -436,7 +436,7 @@ let return_proof ?(allow_partial=false) () = | Proof.HasUnresolvedEvar-> error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in let eff = Evd.eval_side_effects evd in - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 71e2d5820..62ead57f3 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -122,7 +122,7 @@ let compute_name internal id = let define internal id c p univs = let fd = declare_constant ~internal in let id = compute_name internal id in - let ctx = UState.normalize univs in + let ctx = UState.minimize univs in let c = Universes.subst_opt_univs_constr (UState.subst ctx) c in let univs = if p then Polymorphic_const_entry (UState.context ctx) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 655283c20..a4cdc1592 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -218,7 +218,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = end in let avoid = ref Id.Set.empty in let _,_,_,_,sigma = Proof.proof pf in - let sigma = Evd.nf_constraints sigma in + let sigma = Evd.minimize_universes sigma in let rec fill_holes c = match EConstr.kind sigma c with | Evar (e,args) -> diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 1712634da..6a590758f 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -160,7 +160,7 @@ let do_assumptions kind nl l = in let sigma = solve_remaining_evars all_and_fail_flags env sigma Evd.empty in (* The universe constraints come from the whole telescope. *) - let sigma = Evd.nf_constraints sigma in + let sigma = Evd.minimize_universes sigma in let nf_evar c = EConstr.to_constr sigma c in let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> let t = nf_evar t in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 01dbe0a0d..b18a60a1f 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -85,7 +85,7 @@ let interp_definition pl bl poly red_option c ctypopt = evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty in (* universe minimization *) - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in (* Substitute evars and universes, and add parameters. Note: in program mode some evars may remain. *) let ctx = List.map (EConstr.to_rel_decl evd) ctx in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0ff6d9c17..26c6a8cbe 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -72,7 +72,7 @@ let show_top_evars () = let show_universes () = let pfts = Proof_global.give_me_the_proof () in let gls,_,_,_,sigma = Proof.proof pfts in - let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in + let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++ str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx |