aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-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.ml2
-rw-r--r--engine/proofview.mli2
-rw-r--r--engine/proofview_monad.ml2
-rw-r--r--engine/proofview_monad.mli2
-rw-r--r--engine/termops.ml2
-rw-r--r--engine/termops.mli2
-rw-r--r--engine/uState.ml13
-rw-r--r--engine/uState.mli9
20 files changed, 41 insertions, 26 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index df170c8ddc..3d08585a0b 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 7fdc7aac78..585b9cedfb 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 c2f848291b..6ffa4eeb78 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 *)
@@ -809,8 +809,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 86887f3dcc..780ee5ff34 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 *)
@@ -526,7 +526,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 aeaaea7e48..efe828ad57 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 5db373199e..7d9b760a7b 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 17ff898b0f..4fc2489113 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 84eb986845..6be5c6b322 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 97c7c34a56..faff2c916a 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 2e6266cf15..cc63ee21ac 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 *)
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 90be2f90ab..e8a941b081 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 *)
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 697b9a5f15..6242897866 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 *)
diff --git a/engine/termops.mli b/engine/termops.mli
index fd8edafbcf..9ab8e70eca 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 c35f97b2e9..146a386a29 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -381,16 +381,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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 21:53:18 +0000