diff options
Diffstat (limited to 'engine')
-rw-r--r-- | engine/evarutil.ml | 2 | ||||
-rw-r--r-- | engine/evarutil.mli | 2 | ||||
-rw-r--r-- | engine/evd.ml | 7 | ||||
-rw-r--r-- | engine/evd.mli | 6 | ||||
-rw-r--r-- | engine/ftactic.ml | 2 | ||||
-rw-r--r-- | engine/ftactic.mli | 2 | ||||
-rw-r--r-- | engine/geninterp.ml | 2 | ||||
-rw-r--r-- | engine/geninterp.mli | 2 | ||||
-rw-r--r-- | engine/logic_monad.ml | 2 | ||||
-rw-r--r-- | engine/logic_monad.mli | 2 | ||||
-rw-r--r-- | engine/namegen.ml | 2 | ||||
-rw-r--r-- | engine/namegen.mli | 2 | ||||
-rw-r--r-- | engine/proofview.ml | 2 | ||||
-rw-r--r-- | engine/proofview.mli | 2 | ||||
-rw-r--r-- | engine/proofview_monad.ml | 2 | ||||
-rw-r--r-- | engine/proofview_monad.mli | 2 | ||||
-rw-r--r-- | engine/termops.ml | 2 | ||||
-rw-r--r-- | engine/termops.mli | 2 | ||||
-rw-r--r-- | engine/uState.ml | 13 | ||||
-rw-r--r-- | engine/uState.mli | 9 |
20 files changed, 41 insertions, 26 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index df170c8dd..3d08585a0 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 7fdc7aac7..585b9cedf 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 c2f848291..6ffa4eeb7 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 86887f3dc..780ee5ff3 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 aeaaea7e4..efe828ad5 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 5db373199..7d9b760a7 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 cfca95d3e..9964433a8 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 b70671a2d..9a925dcd8 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 17ff898b0..4fc248911 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 dd122cca0..aaebe4c1b 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 84eb98684..6be5c6b32 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 97c7c34a5..faff2c916 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 2e6266cf1..cc63ee21a 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 90be2f90a..e8a941b08 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 6f52b3ee9..1b737b6f4 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 637414cce..554583421 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 697b9a5f1..624289786 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 fd8edafbc..9ab8e70ec 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 c35f97b2e..146a386a2 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 0cdc6277a..3776e4c9f 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 |