aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml2
-rw-r--r--engine/eConstr.mli2
-rw-r--r--engine/evarutil.ml2
-rw-r--r--engine/evarutil.mli2
-rw-r--r--engine/evd.ml7
-rw-r--r--engine/evd.mli6
-rw-r--r--engine/ftactic.ml2
-rw-r--r--engine/ftactic.mli2
-rw-r--r--engine/geninterp.ml2
-rw-r--r--engine/geninterp.mli2
-rw-r--r--engine/logic_monad.ml2
-rw-r--r--engine/logic_monad.mli2
-rw-r--r--engine/namegen.ml2
-rw-r--r--engine/namegen.mli2
-rw-r--r--engine/proofview.ml11
-rw-r--r--engine/proofview.mli4
-rw-r--r--engine/proofview_monad.ml2
-rw-r--r--engine/proofview_monad.mli2
-rw-r--r--engine/termops.ml4
-rw-r--r--engine/termops.mli2
-rw-r--r--engine/uState.ml13
-rw-r--r--engine/uState.mli9
-rw-r--r--engine/universes.ml91
-rw-r--r--engine/universes.mli13
24 files changed, 59 insertions, 129 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 078f2fc333..7b879a8031 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 07a4dc8e23..4dbf6c18a3 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index e8d184632e..2afc12cd36 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 90c5c3dc0d..a8b6b5861c 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/engine/evd.ml b/engine/evd.ml
index bf1e052b63..cfc9aa6351 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -780,8 +780,9 @@ let new_sort_variable ?loc ?name rigid d =
let add_global_univ d u =
{ d with universes = UState.add_global_univ d.universes u }
-let make_flexible_variable evd b u =
- { evd with universes = UState.make_flexible_variable evd.universes b u }
+let make_flexible_variable evd ~algebraic u =
+ { evd with universes =
+ UState.make_flexible_variable evd.universes ~algebraic u }
let make_evar_universe_context e l =
let uctx = UState.make (Environ.universes e) in
diff --git a/engine/evd.mli b/engine/evd.mli
index 86755c360b..3f00a3b0b2 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -522,7 +522,9 @@ val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_
val add_global_univ : evar_map -> Univ.Level.t -> evar_map
val universe_rigidity : evar_map -> Univ.Level.t -> rigid
-val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
+val make_flexible_variable : evar_map -> algebraic:bool -> Univ.universe_level -> evar_map
+(** See [UState.make_flexible_variable] *)
+
val is_sort_variable : evar_map -> sorts -> Univ.universe_level option
(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is
not a local sort variable declared in [evm] *)
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index 68368e38fa..8e4c5f2206 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/engine/ftactic.mli b/engine/ftactic.mli
index 97bebe9da8..c108c0c2ea 100644
--- a/engine/ftactic.mli
+++ b/engine/ftactic.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/engine/geninterp.ml b/engine/geninterp.ml
index cfca95d3e6..9964433a80 100644
--- a/engine/geninterp.ml
+++ b/engine/geninterp.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
index b70671a2d9..9a925dcd89 100644
--- a/engine/geninterp.mli
+++ b/engine/geninterp.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 6e821ea5aa..bf1b3e0e86 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index dd122cca0f..aaebe4c1b0 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 783085654e..a75fe721f7 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/engine/namegen.mli b/engine/namegen.mli
index 058b1c228b..14846a9184 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 39ef65dab1..b4e2160f4e 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -1072,13 +1072,6 @@ module Goal = struct
end
end
- exception NotExactlyOneSubgoal
- let _ = CErrors.register_handler begin function
- | NotExactlyOneSubgoal ->
- CErrors.user_err (Pp.str"Not exactly one subgoal.")
- | _ -> raise CErrors.Unhandled
- end
-
let enter_one f =
let open Proof in
Comb.get >>= function
@@ -1090,7 +1083,7 @@ module Goal = struct
let (e, info) = CErrors.push e in
tclZERO ~info e
end
- | _ -> tclZERO NotExactlyOneSubgoal
+ | _ -> assert false (* unsatisfied not-exactly-one-goal precondition *)
let goals =
Pv.get >>= fun step ->
diff --git a/engine/proofview.mli b/engine/proofview.mli
index aae25b6f8f..530204501e 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -498,7 +498,7 @@ module Goal : sig
val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
(** Like {!enter}, but assumes exactly one goal under focus, raising *)
- (** an error otherwise. *)
+ (** a fatal error otherwise. *)
val enter_one : ([ `LZ ] t -> 'a tactic) -> 'a tactic
(** Recover the list of current goals under focus, without evar-normalization.
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 6f52b3ee90..1b737b6f4d 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index 637414cce7..554583421b 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/engine/termops.ml b/engine/termops.ml
index 3eef71b2d0..1aba2bbdd1 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -906,7 +906,7 @@ let collect_vars sigma c =
aux Id.Set.empty c
let vars_of_global_reference env gr =
- let c, _ = Universes.unsafe_constr_of_global gr in
+ let c, _ = Global.constr_of_global_in_context env gr in
vars_of_global (Global.env ()) c
(* Tests whether [m] is a subterm of [t]:
diff --git a/engine/termops.mli b/engine/termops.mli
index 58837ba033..c19a2d15a5 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/engine/uState.ml b/engine/uState.ml
index 0973ca457f..63bd247d56 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -384,16 +384,21 @@ let add_global_univ uctx u =
uctx_initial_universes = initial;
uctx_universes = univs }
-let make_flexible_variable ctx b u =
- let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in
+let make_flexible_variable ctx ~algebraic u =
+ let {uctx_local = cstrs; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in
let uvars' = Univ.LMap.add u None uvars in
let avars' =
- if b then
+ if algebraic then
let uu = Univ.Universe.make u in
let substu_not_alg u' v =
Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v
in
- if not (Univ.LMap.exists substu_not_alg uvars)
+ let has_upper_constraint () =
+ Univ.Constraint.exists
+ (fun (l,d,r) -> d == Univ.Lt && Univ.Level.equal l u)
+ (Univ.ContextSet.constraints cstrs)
+ in
+ if not (Univ.LMap.exists substu_not_alg uvars || has_upper_constraint ())
then Univ.LSet.add u avars else avars
else avars
in
diff --git a/engine/uState.mli b/engine/uState.mli
index 0cdc6277a5..3776e4c9fd 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -92,7 +92,14 @@ val emit_side_effects : Safe_typing.private_constants -> t -> t
val new_univ_variable : ?loc:Loc.t -> rigid -> string option -> t -> t * Univ.Level.t
val add_global_univ : t -> Univ.Level.t -> t
-val make_flexible_variable : t -> bool -> Univ.Level.t -> t
+
+(** [make_flexible_variable g algebraic l]
+
+ Turn the variable [l] flexible, and algebraic if [algebraic] is true
+ and [l] can be. That is if there are no strict upper constraints on
+ [l] and and it does not appear in the instance of any non-algebraic
+ universe. Otherwise the variable is just made flexible. *)
+val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t
val is_sort_variable : t -> Sorts.t -> Univ.Level.t option
diff --git a/engine/universes.ml b/engine/universes.ml
index dd6a69d9f9..08461a2186 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -282,28 +282,27 @@ let new_Type dp = mkType (new_univ dp)
let new_Type_sort dp = Type (new_univ dp)
let fresh_universe_instance ctx =
- Instance.subst_fn (fun _ -> new_univ_level (Global.current_dirpath ()))
- (AUContext.instance ctx)
+ let init _ = new_univ_level (Global.current_dirpath ()) in
+ Instance.of_array (Array.init (AUContext.size ctx) init)
let fresh_instance_from_context ctx =
let inst = fresh_universe_instance ctx in
- let constraints = UContext.constraints (subst_instance_context inst ctx) in
+ let constraints = AUContext.instantiate inst ctx in
inst, constraints
let fresh_instance ctx =
let ctx' = ref LSet.empty in
- let inst =
- Instance.subst_fn (fun v ->
- let u = new_univ_level (Global.current_dirpath ()) in
- ctx' := LSet.add u !ctx'; u)
- (AUContext.instance ctx)
+ let init _ =
+ let u = new_univ_level (Global.current_dirpath ()) in
+ ctx' := LSet.add u !ctx'; u
+ in
+ let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
in !ctx', inst
let existing_instance ctx inst =
let () =
- let a1 = Instance.to_array inst
- and a2 = Instance.to_array (AUContext.instance ctx) in
- let len1 = Array.length a1 and len2 = Array.length a2 in
+ let len1 = Array.length (Instance.to_array inst)
+ and len2 = AUContext.size ctx in
if not (len1 == len2) then
CErrors.user_err ~hdr:"Universes"
(str "Polymorphic constant expected " ++ int len2 ++
@@ -317,12 +316,9 @@ let fresh_instance_from ctx inst =
| Some inst -> existing_instance ctx inst
| None -> fresh_instance ctx
in
- let constraints = UContext.constraints (subst_instance_context inst ctx) in
+ let constraints = AUContext.instantiate inst ctx in
inst, (ctx', constraints)
-let unsafe_instance_from ctx =
- (Univ.AUContext.instance ctx, Univ.instantiate_univ_context ctx)
-
(** Fresh universe polymorphic construction *)
let fresh_constant_instance env c inst =
@@ -359,34 +355,6 @@ let fresh_constructor_instance env (ind,i) inst =
let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
(((ind,i),inst), ctx)
-let unsafe_constant_instance env c =
- let cb = lookup_constant c env in
- match cb.Declarations.const_universes with
- | Declarations.Monomorphic_const _ ->
- ((c,Instance.empty), UContext.empty)
- | Declarations.Polymorphic_const auctx ->
- let inst, ctx = unsafe_instance_from auctx in ((c, inst), ctx)
-
-let unsafe_inductive_instance env ind =
- let mib, mip = Inductive.lookup_mind_specif env ind in
- match mib.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ -> ((ind,Instance.empty), UContext.empty)
- | Declarations.Polymorphic_ind auctx ->
- let inst, ctx = unsafe_instance_from auctx in ((ind,inst), ctx)
- | Declarations.Cumulative_ind acumi ->
- let inst, ctx = unsafe_instance_from (ACumulativityInfo.univ_context acumi) in
- ((ind,inst), ctx)
-
-let unsafe_constructor_instance env (ind,i) =
- let mib, mip = Inductive.lookup_mind_specif env ind in
- match mib.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ -> (((ind, i),Instance.empty), UContext.empty)
- | Declarations.Polymorphic_ind auctx ->
- let inst, ctx = unsafe_instance_from auctx in (((ind, i),inst), ctx)
- | Declarations.Cumulative_ind acumi ->
- let inst, ctx = unsafe_instance_from (ACumulativityInfo.univ_context acumi) in
- (((ind, i),inst), ctx)
-
open Globnames
let fresh_global_instance ?names env gr =
@@ -411,19 +379,6 @@ let fresh_inductive_instance env sp =
let fresh_constructor_instance env sp =
fresh_constructor_instance env sp None
-let unsafe_global_instance env gr =
- match gr with
- | VarRef id -> mkVar id, UContext.empty
- | ConstRef sp ->
- let c, ctx = unsafe_constant_instance env sp in
- mkConstU c, ctx
- | ConstructRef sp ->
- let c, ctx = unsafe_constructor_instance env sp in
- mkConstructU c, ctx
- | IndRef sp ->
- let c, ctx = unsafe_inductive_instance env sp in
- mkIndU c, ctx
-
let constr_of_global gr =
let c, ctx = fresh_global_instance (Global.env ()) gr in
if not (Univ.ContextSet.is_empty ctx) then
@@ -438,9 +393,6 @@ let constr_of_global gr =
let constr_of_reference = constr_of_global
-let unsafe_constr_of_global gr =
- unsafe_global_instance (Global.env ()) gr
-
let constr_of_global_univ (gr,u) =
match gr with
| VarRef id -> mkVar id
@@ -514,25 +466,6 @@ let type_of_reference env r =
let type_of_global t = type_of_reference (Global.env ()) t
-let unsafe_type_of_reference env r =
- match r with
- | VarRef id -> Environ.named_type id env
- | ConstRef c ->
- let cb = Environ.lookup_constant c env in
- Typeops.type_of_constant_type env cb.const_type
-
- | IndRef ind ->
- let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
- let (_, inst), _ = unsafe_inductive_instance env ind in
- Inductive.type_of_inductive env (specif, inst)
-
- | ConstructRef (ind, _ as cstr) ->
- let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- let (_, inst), _ = unsafe_inductive_instance env ind in
- Inductive.type_of_constructor (cstr,inst) specif
-
-let unsafe_type_of_global t = unsafe_type_of_reference (Global.env ()) t
-
let fresh_sort_in_family env = function
| InProp -> prop_sort, ContextSet.empty
| InSet -> set_sort, ContextSet.empty
diff --git a/engine/universes.mli b/engine/universes.mli
index 6c2cee485c..0f6e419d00 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -189,22 +189,11 @@ val constr_of_global : Globnames.global_reference -> constr
(** ** DEPRECATED ** synonym of [constr_of_global] *)
val constr_of_reference : Globnames.global_reference -> constr
-(** [unsafe_constr_of_global gr] turns [gr] into a constr, works on polymorphic
- references by taking the original universe instance that is not recorded
- anywhere. The constraints are forgotten as well. DO NOT USE in new code. *)
-val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_context
-
(** Returns the type of the global reference, by creating a fresh instance of polymorphic
references and computing their instantiated universe context. (side-effect on the
universe counter, use with care). *)
val type_of_global : Globnames.global_reference -> types in_universe_context_set
-(** [unsafe_type_of_global gr] returns [gr]'s type, works on polymorphic
- references by taking the original universe instance that is not recorded
- anywhere. The constraints are forgotten as well.
- USE with care. *)
-val unsafe_type_of_global : Globnames.global_reference -> types
-
(** Full universes substitutions into terms *)
val nf_evars_and_universes_opt_subst : (existential -> constr option) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 17:01:25 +0000