From 03a71a241f8d05f6a86f3c8f3c2146c4db378f7b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 13 Jun 2016 18:42:01 +0200
Subject: Univs: more robust Universe/Constraint decls #4816

This fixes the declarations of constraints, universes
and assumptions:
- global constraints can refer to global universes only,
- polymorphic universes, constraints and assumptions can only be
  declared inside sections, when all the section's
  variables/universes are polymorphic as well.
- monomorphic assumptions may only be declared in section contexts
  which are not parameterized by polymorphic universes/assumptions.

Add fix for part 1 of bug #4816
---
 pretyping/pretyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index efc42aab76..378294c984 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -143,7 +143,7 @@ let interp_universe_level_name evd (loc,s) =
       with Not_found ->
 	try 
 	  let id = try Id.of_string s with _ -> raise Not_found in
-	  evd, Idmap.find id names
+          evd, snd (Idmap.find id names)
 	with Not_found -> 
 	  if not (is_strict_universe_declarations ()) then
   	    new_univ_level_variable ~loc ~name:s univ_rigid evd
-- 
cgit v1.2.3