From da178a880e3ace820b41d38b191d3785b82991f5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 1 Jul 2010 17:21:14 +0200
Subject: Imported Upstream version 8.2pl2+dfsg

---
 interp/constrextern.ml |  3 +--
 interp/constrintern.ml | 21 ++++++++++++---------
 2 files changed, 13 insertions(+), 11 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f99af68e..99bcf159 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrextern.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: constrextern.ml 12495 2009-11-11 12:10:44Z herbelin $ *)
 
 (*i*)
 open Pp
@@ -363,7 +363,6 @@ let bind_env (sigma,sigmalist as fullsigma) var v =
 let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
   | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
   | PatVar (_,Anonymous), AHole _ -> sigma
-  | a, AHole _ -> sigma
   | PatCstr (loc,(ind,_ as r1),args1,_), _ ->
       let nparams =
 	(fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8d6a92a2..c8faf911 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: constrintern.ml 11739 2009-01-02 19:33:19Z herbelin $ *)
+(* $Id: constrintern.ml 13131 2010-06-13 18:45:17Z herbelin $ *)
 
 open Pp
 open Util
@@ -450,8 +450,8 @@ let rec simple_adjust_scopes n = function
 let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) =
   let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
   let npar = mib.Declarations.mind_nparams in
-  snd (list_chop (List.length pl1 + npar)
-    (simple_adjust_scopes (npar + List.length pl2)
+  snd (list_chop (npar + List.length pl1)
+    (simple_adjust_scopes (npar + List.length pl1 + List.length pl2)
       (find_arguments_scope (ConstructRef cstr))))
 
 (**********************************************************************)
@@ -526,6 +526,7 @@ let error_invalid_pattern_notation loc =
 
 let chop_aconstr_constructor loc (ind,k) args =
   let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
+  if nparams > List.length args then error_invalid_pattern_notation loc;
   let params,args = list_chop nparams args in
   List.iter (function AHole _ -> ()
     | _ -> error_invalid_pattern_notation loc) params;
@@ -728,8 +729,7 @@ let locate_if_isevar loc na = function
 let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
   if List.mem id indnames then
     errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++
-    pr_id id ++ strbrk " must not be used as a bound variable in the type \
-of its constructor.")
+    pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
 
 let push_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) = function
   | Anonymous -> 
@@ -1060,15 +1060,17 @@ let internalise sigma globalenv env allow_patvar lvar c =
     | CLetTuple (loc, nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
         let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
-        let env'' = List.fold_left (push_name_env lvar) env ids in
-        let p' = Option.map (intern_type env'') po in
+        let p' = Option.map (fun p ->
+          let env'' = List.fold_left (push_name_env lvar) env ids in
+	  intern_type env'' p) po in
         RLetTuple (loc, nal, (na', p'), b',
                    intern (List.fold_left (push_name_env lvar) env nal) c)
     | CIf (loc, c, (na,po), b1, b2) ->
 	let env' = reset_tmp_scope env in
         let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
-        let env'' = List.fold_left (push_name_env lvar) env ids in
-        let p' = Option.map (intern_type env'') po in
+        let p' = Option.map (fun p ->
+          let env'' = List.fold_left (push_name_env lvar) env ids in
+	  intern_type env'' p) po in
         RIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole (loc, k) -> 
 	RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true))
@@ -1147,6 +1149,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	[], None in
     let na = match tm', na with
       | RVar (_,id), None when Idset.mem id vars -> Name id
+      | RRef (loc, VarRef id), None -> Name id
       | _, None -> Anonymous
       | _, Some na -> na in
     (tm',(na,typ)), na::ids
-- 
cgit v1.2.3