From 88afd8a9853c772b6b1681c7ae208e55e7daacbe Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 19 Nov 2017 08:11:07 +0100 Subject: [api] Deprecate Term destructors, move to Constr We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`. --- engine/univops.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/univops.ml') diff --git a/engine/univops.ml b/engine/univops.ml index 9dc138eb8..d498b2e0d 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -6,8 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Constr open Univ +open Constr let universes_of_constr c = let rec aux s c = @@ -15,7 +15,7 @@ let universes_of_constr c = | Const (_, u) | Ind (_, u) | Construct (_, u) -> LSet.fold LSet.add (Instance.levels u) s | Sort u when not (Sorts.is_small u) -> - let u = Term.univ_of_sort u in + let u = Sorts.univ_of_sort u in LSet.fold LSet.add (Universe.levels u) s | _ -> Constr.fold aux s c in aux LSet.empty c -- cgit v1.2.3