From 1c450e282d8e6ae37f687c545776939f2d975cf3 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 26 Oct 2008 21:45:47 +0000
Subject: Correct enormous bug in interpretation of generalized binders: it
 simply dropped all bindings appearing before it :) Bug found by Marc Lasson.

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

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ef7ad36f12..dd94bf42d1 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -717,7 +717,8 @@ let intern_local_binder_aux intern intern_type lvar ((ids,unb,ts,sc as env),bl)
 		((name_fold Idset.add na ids,unb,ts,sc), (na,k,None,ty)::bl))
 	      (env,bl) nal
       | Generalized (b,b',t) ->
-	  intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty)
+	  let env, b = intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty in
+	    env, b @ bl)
   | LocalRawDef((loc,na),def) ->
       ((name_fold Idset.add na ids,unb,ts,sc),
       (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
-- 
cgit v1.2.3