From 66acf05f6fd0a35b7d9a0d425983c36dbe2cc992 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 5 Sep 2014 20:27:37 +0200
Subject: Fix checker treatment of inductives using subst_instances instead of
 subst_univs_levels.

---
 kernel/univ.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 202f6232da..fd65d7de50 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -2003,7 +2003,6 @@ let subst_univs_constraints subst csts =
     (fun c cstrs -> subst_univs_constraint subst c cstrs)
     csts Constraint.empty 
 
-
 let subst_instance_level s l =
   match l.Level.data with
   | Level.Var n -> s.(n) 
-- 
cgit v1.2.3