From 70661f61a23954db18ff4836778945ae235157b2 Mon Sep 17 00:00:00 2001
From: msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 3 Jun 2009 17:54:27 +0000
Subject: Ensure the precondition of the partial function [list_chop] holds
 before calling it.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12162 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/prettyp.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index d24f2dd6f..f00e5f0a1 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -107,8 +107,9 @@ let need_expansion impl ref =
   let typ = Global.type_of_global ref in
   let ctx = (prod_assum typ) in
   let nprods = List.length (List.filter (fun (_,b,_) -> b=None) ctx) in
-  impl <> [] & let _,lastimpl = list_chop nprods impl in
-  List.filter is_status_implicit lastimpl <> []
+  impl <> [] & List.length impl >= nprods &
+    let _,lastimpl = list_chop nprods impl in
+      List.filter is_status_implicit lastimpl <> []
 
 type opacity =
   | FullyOpaque
-- 
cgit v1.2.3