Correction bug 1172 + correction en passant de la taille des paramètres de famille

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9032 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 22 insertions, 16 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index dae19f7969..857d3400a4 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -406,7 +406,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  List.iter 
 	    (option_iter 
 	       (fun kn -> if Cset.mem kn !projs then add_projection n kn))
-	    (lookup_structure ip).s_PROJ 
+	    (lookup_projections ip)
 	with Not_found -> ()
 	end; 
 	Record field_glob
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 2235be4a08..b6b1c7b68a 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -474,7 +474,7 @@ let kind_of_global r =
   match r with
   | Ln.IndRef kn | Ln.ConstructRef (kn,_) -> 
       let isrecord =
-	try let _ = Recordops.lookup_structure kn in true
+	try let _ = Recordops.lookup_projections kn in true
         with Not_found -> false in
       kind_of_inductive isrecord (fst kn)
   | Ln.VarRef id -> kind_of_variable id
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 855fcb329f..57f2c6a892 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -554,6 +554,11 @@ let rec local_binders_length = function
   | LocalRawDef _::bl -> 1 + local_binders_length bl
   | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl
 
+let rec local_assums_length = function
+  | [] -> 0
+  | LocalRawDef _::bl -> local_binders_length bl
+  | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl
+
 let names_of_local_assums bl =
   List.flatten (List.map (function LocalRawAssum(l,_)->l|_->[]) bl)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index e06a482159..e1d35bb274 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -159,6 +159,9 @@ val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
 (* Includes let binders *)
 val local_binders_length : local_binder list -> int
 
+(* Excludes let binders *)
+val local_assums_length : local_binder list -> int
+
 (* Does not take let binders into account *)
 val names_of_local_assums : local_binder list -> name located list
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 983f58f9cd..5fffeb7093 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -32,7 +32,7 @@ open Mod_subst
 
 type struc_typ = {
   s_CONST : identifier; 
-  s_PARAM : int;
+  s_EXPECTEDPARAM : int;
   s_PROJKIND : bool list;
   s_PROJ : constant option list }
 
@@ -44,7 +44,7 @@ let option_fold_right f p e = match p with Some a -> f a e | None -> e
 let load_structure i (_,(ind,id,kl,projs)) =
   let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
   let struc =
-    { s_CONST = id; s_PARAM = n; s_PROJ = projs; s_PROJKIND = kl } in
+    { s_CONST = id; s_EXPECTEDPARAM = n; s_PROJ = projs; s_PROJKIND = kl } in
   structure_table := Indmap.add ind struc !structure_table;
   projection_table := 
     List.fold_right (option_fold_right (fun proj -> Cmap.add proj struc))
@@ -83,8 +83,10 @@ let declare_structure (s,c,_,kl,pl) =
 
 let lookup_structure indsp = Indmap.find indsp !structure_table
 
+let lookup_projections indsp = (lookup_structure indsp).s_PROJ
+
 let find_projection_nparams = function
-  | ConstRef cst -> (Cmap.find cst !projection_table).s_PARAM
+  | ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM
   | _ -> raise Not_found
 
 
@@ -134,7 +136,7 @@ let compute_canonical_projections (con,ind) =
   let lt,t = Reductionops.splay_lambda (Global.env()) Evd.empty c in
   let lt = List.rev (List.map snd lt) in
   let args = snd (decompose_app t) in
-  let { s_PARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in
+  let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in
   let params, projs = list_chop p args in
   let lpj = keep_true_projections lpj kl in
   let lps = List.combine lpj projs in
@@ -202,7 +204,8 @@ let check_and_decompose_canonical_structure ref =
     | Construct (indsp,1) -> indsp
     | _ -> error_not_structure ref in
   let s = try lookup_structure indsp with Not_found -> error_not_structure ref in
-  if s.s_PARAM + List.length s.s_PROJ > Array.length args then
+  let ntrue_projs = List.length (List.filter (fun x -> x) s.s_PROJKIND) in
+  if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
     error_not_structure ref;
   (sp,indsp)
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index d6f90e11ed..f917909e22 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -21,18 +21,13 @@ open Library
 (*s A structure S is a non recursive inductive type with a single
    constructor (the name of which defaults to Build_S) *)
 
-type struc_typ = {
-  s_CONST : identifier; 
-  s_PARAM : int;
-  s_PROJKIND : bool list;
-  s_PROJ : constant option list }
-
 val declare_structure : 
   inductive * identifier * int * bool list * constant option list -> unit
 
-(* [lookup_structure isp] returns the infos associated to inductive path
-   [isp] if it corresponds to a structure, otherwise fails with [Not_found] *)
-val lookup_structure : inductive -> struc_typ
+(* [lookup_projections isp] returns the projections associated to the
+   inductive path [isp] if it corresponds to a structure, otherwise
+   it fails with [Not_found] *)
+val lookup_projections : inductive -> constant option list
 
 (* raise [Not_found] if not a projection *)
 val find_projection_nparams : global_reference -> int