From d0d5ddd6ecc78813a0adf6a4df863b2fa5cce743 Mon Sep 17 00:00:00 2001
From: gmelquio
Date: Wed, 6 Jan 2010 13:14:45 +0000
Subject: Allowed handling of partly-applied record constructors. (Fix for bug
 #2196.)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12632 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 550155ee30..65976a03f9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -663,7 +663,11 @@ let rec extern inctx scopes vars r =
 		 let projs = struc.Recordops.s_PROJ in
 		 let locals = struc.Recordops.s_PROJKIND in
 		 let rec cut args n =
-		   if n = 0 then args else cut (List.tl args) (n - 1) in
+		   if n = 0 then args
+		   else
+		     match args with
+		     | [] -> raise No_match
+		     | _ :: t -> cut t (n - 1) in
 		 let args = cut args struc.Recordops.s_EXPECTEDPARAM in
 		 let rec ip projs locs args acc =
 		   match projs with
-- 
cgit v1.2.3