aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/07906-univs-of-constr.sh9
-rw-r--r--engine/eConstr.ml13
-rw-r--r--engine/eConstr.mli2
-rw-r--r--engine/univops.ml15
-rw-r--r--engine/univops.mli4
-rw-r--r--plugins/setoid_ring/newring.ml3
-rw-r--r--proofs/proof_global.ml5
-rw-r--r--vernac/classes.ml5
-rw-r--r--vernac/comAssumption.ml2
-rw-r--r--vernac/comDefinition.ml2
-rw-r--r--vernac/comFixpoint.ml5
-rw-r--r--vernac/obligations.ml5
12 files changed, 26 insertions, 44 deletions
diff --git a/dev/ci/user-overlays/07906-univs-of-constr.sh b/dev/ci/user-overlays/07906-univs-of-constr.sh
new file mode 100644
index 000000000..071665087
--- /dev/null
+++ b/dev/ci/user-overlays/07906-univs-of-constr.sh
@@ -0,0 +1,9 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "7906" ] || [ "$CI_BRANCH" = "univs-of-constr-noseff" ]; then
+ Equations_CI_BRANCH=fix-univs-of-constr
+ Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git
+
+ Elpi_CI_BRANCH=fix-universes-of-constr
+ Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git
+fi
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 6810626ad..005ef1635 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -592,25 +592,14 @@ let eq_constr_universes_proj env sigma m n =
let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in
if res then Some !cstrs else None
-let universes_of_constr env sigma c =
+let universes_of_constr sigma c =
let open Univ in
- let open Declarations in
let rec aux s c =
match kind sigma c with
| Const (c, u) ->
- begin match (Environ.lookup_constant c env).const_universes with
- | Polymorphic_const _ ->
LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
- | Monomorphic_const (univs, _) ->
- LSet.union s univs
- end
| Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
- begin match (Environ.lookup_mind mind env).mind_universes with
- | Cumulative_ind _ | Polymorphic_ind _ ->
LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
- | Monomorphic_ind (univs,_) ->
- LSet.union s univs
- end
| Sort u ->
let sort = ESorts.kind sigma u in
if Sorts.is_small sort then s
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index e9d3e782b..913825a9f 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -232,7 +232,7 @@ val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
(** Gather the universes transitively used in the term, including in the
type of evars appearing in it. *)
-val universes_of_constr : Environ.env -> Evd.evar_map -> t -> Univ.LSet.t
+val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t
(** {6 Substitutions} *)
diff --git a/engine/univops.ml b/engine/univops.ml
index 3fd518490..7f9672f82 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -11,24 +11,13 @@
open Univ
open Constr
-let universes_of_constr env c =
- let open Declarations in
- let rec aux s c =
+let universes_of_constr c =
+ let rec aux s c =
match kind c with
| Const (c, u) ->
- begin match (Environ.lookup_constant c env).const_universes with
- | Polymorphic_const _ ->
LSet.fold LSet.add (Instance.levels u) s
- | Monomorphic_const (univs, _) ->
- LSet.union s univs
- end
| Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
- begin match (Environ.lookup_mind mind env).mind_universes with
- | Cumulative_ind _ | Polymorphic_ind _ ->
LSet.fold LSet.add (Instance.levels u) s
- | Monomorphic_ind (univs,_) ->
- LSet.union s univs
- end
| Sort u when not (Sorts.is_small u) ->
let u = Sorts.univ_of_sort u in
LSet.fold LSet.add (Universe.levels u) s
diff --git a/engine/univops.mli b/engine/univops.mli
index 0b37ab975..57a53597b 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -11,8 +11,8 @@
open Constr
open Univ
-(** The universes of monomorphic constants appear. *)
-val universes_of_constr : Environ.env -> constr -> LSet.t
+(** Return the set of all universes appearing in [constr]. *)
+val universes_of_constr : constr -> LSet.t
(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
the universes in [keep]. The constraints [csts] are adjusted so
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 84b29a0bf..e4d17f250 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -148,8 +148,7 @@ let ic_unsafe c = (*FIXME remove *)
let decl_constant na univs c =
let open Constr in
- let env = Global.env () in
- let vars = Univops.universes_of_constr env c in
+ let vars = Univops.universes_of_constr c in
let univs = Univops.restrict_universe_context univs vars in
let univs = Monomorphic_const_entry univs in
mkConst(declare_constant (Id.of_string na)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 3120c97b5..47c9c51ee 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -348,9 +348,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
not (Safe_typing.empty_private_constants = eff))
in
let typ = if allow_deferred then t else nf t in
- let env = Global.env () in
- let used_univs_body = Univops.universes_of_constr env body in
- let used_univs_typ = Univops.universes_of_constr env typ in
+ let used_univs_body = Univops.universes_of_constr body in
+ let used_univs_typ = Univops.universes_of_constr typ in
if allow_deferred then
let initunivs = UState.const_univ_entry ~poly initial_euctx in
let ctx = constrain_variables universes in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 382d18b09..26d105ecf 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -116,9 +116,8 @@ let instance_hook k info global imps ?hook cst =
let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype =
let kind = IsDefinition Instance in
let sigma =
- let env = Global.env () in
- let levels = Univ.LSet.union (Univops.universes_of_constr env termtype)
- (Univops.universes_of_constr env term) in
+ let levels = Univ.LSet.union (Univops.universes_of_constr termtype)
+ (Univops.universes_of_constr term) in
Evd.restrict_universe_context sigma levels
in
let uctx = Evd.check_univ_decl ~poly sigma decl in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index a8ac52846..750ed35cb 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -163,7 +163,7 @@ let do_assumptions kind nl l =
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
- let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in
+ let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in
uvars, (coe,t,imps))
Univ.LSet.empty l
in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index f55c852c0..a8d794642 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -93,7 +93,7 @@ let interp_definition pl bl poly red_option c ctypopt =
let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd ty) ctx) tyopt in
(* Keep only useful universes. *)
let uvars_fold uvars c =
- Univ.LSet.union uvars (universes_of_constr env evd (of_constr c))
+ Univ.LSet.union uvars (universes_of_constr evd (of_constr c))
in
let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in
let evd = Evd.restrict_universe_context evd uvars in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 1d1cc62de..37258c2d4 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -262,7 +262,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
let env = Global.env() in
let indexes = search_guard env indexes fixdecls in
let fiximps = List.map (fun (n,r,p) -> r) fiximps in
- let vars = Univops.universes_of_constr env (mkFix ((indexes,0),fixdecls)) in
+ let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
let fixdecls =
List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
let evd = Evd.from_ctx ctx in
@@ -295,8 +295,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
let fixdefs = List.map Option.get fixdefs in
let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
- let env = Global.env () in
- let vars = Univops.universes_of_constr env (List.hd fixdecls) in
+ let vars = Univops.universes_of_constr (List.hd fixdecls) in
let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
let evd = Evd.from_ctx ctx in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index e0b1349f7..fa6a9adf1 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -480,10 +480,9 @@ let declare_definition prg =
let fix_exn = Hook.get get_fix_exn () in
let typ = nf typ in
let body = nf body in
- let env = Global.env () in
let uvars = Univ.LSet.union
- (Univops.universes_of_constr env typ)
- (Univops.universes_of_constr env body) in
+ (Univops.universes_of_constr typ)
+ (Univops.universes_of_constr body) in
let uctx = UState.restrict prg.prg_ctx uvars in
let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in
let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-09 19:26:44 +0000