From b6733f0507e3e04fb6130b3f82a79e8835e1062f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 31 May 2017 00:30:00 +0200
Subject: Bump year in headers.

---
 engine/evd.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index 86887f3dcc..5d6d1a5b9d 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        *)
-- 
cgit v1.2.3


From 36f3ae391ee188edb9d858d8832d7fd611db0482 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 21 Feb 2017 12:56:28 +0100
Subject: Univs: fix bug #5365, generation of u+k <= v constraints

Use an explicit label ~algebraic for make_flexible_variable as well.
---
 engine/evd.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index 86887f3dcc..93d4a9d152 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -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] *)
-- 
cgit v1.2.3