From f72a67569ec8cb9160d161699302b67919da5686 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 27 Jul 2017 14:54:41 +0200
Subject: Allow declaring universe constraints at definition level.

Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof.  By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.

Declarations of universe binders and constraints also works for
monomorphic definitions.
---
 plugins/ltac/tacentries.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index cf676f598f..a8d518fbd8 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -216,7 +216,6 @@ let interp_prod_item = function
       assert (String.equal s "tactic");
       begin match Tacarg.wit_tactic with
       | ExtraArg tag -> ArgT.Any tag
-      | _ -> assert false
       end
     in
     let symbol = interp_entry_name interp symbol in
-- 
cgit v1.2.3


From cd29948855c2cbd3f4065170e41f8dbe625e1921 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 9 Sep 2017 14:00:42 +0200
Subject: Don't lose names in UState.universe_context.

We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
---
 plugins/ltac/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 75b665aad9..3d01cbe8dd 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1884,7 +1884,7 @@ let declare_projection n instance_id r =
     in it_mkProd_or_LetIn ccl ctx
   in
   let typ = it_mkProd_or_LetIn typ ctx in
-  let pl, ctx = Evd.universe_context sigma in
+  let pl, ctx = Evd.universe_context ~names:[] ~extensible:true sigma in
   let typ = EConstr.to_constr sigma typ in
   let term = EConstr.to_constr sigma term in
   let cst = 
-- 
cgit v1.2.3