From 784d82dc1a709c4c262665a4cd4eb0b1bd1487a0 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Mon, 13 Jun 2016 18:36:58 +0200
Subject: Univs: fix for part #2 of bug #4816.

Check that the polymorphic status of everything that
is parameterized in nested sections is coherent.
---
 library/lib.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index e4617cafb..f6b4a2458 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -417,7 +417,7 @@ let add_section_variable id impl poly ctx =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
-       check_same_poly poly vars;
+       List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab;
        sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
 
 let add_section_context ctx =
-- 
cgit v1.2.3