Fix treatment of {struct x} annotations in presence of generalized

binders.


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

3 files changed, 17 insertions, 10 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ecaba603d2..ceb0748fee 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1047,12 +1047,11 @@ let internalise sigma globalenv env allow_patvar lvar c =
         let idl = Array.map
           (fun (id,(n,order),bl,ty,bd) ->
 	     let intern_ro_arg f =
-               let idx = Option.default 0 (index_of_annot bl n) in
-	       let before, after = list_chop idx bl in
+	       let before, after = split_at_annot bl n in
 	       let ((ids',_,_,_) as env',rbefore) =
 		 List.fold_left intern_local_binder (env,[]) before in
 	       let ro = f (intern (ids', unb, tmp_scope, scopes)) in
-	       let n' = Option.map (fun _ -> List.length before) n in
+	       let n' = Option.map (fun _ -> List.length rbefore) n in
 		 n', ro, List.fold_left intern_local_binder (env',rbefore) after
 	     in
 	     let n, ro, ((ids',_,_,_),rbl) =
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 5fade008cf..e9a81f09ca 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -908,17 +908,25 @@ let coerce_to_name = function
 
 (* Interpret the index of a recursion order annotation *)
 
-let index_of_annot bl na =
+let split_at_annot bl na =
   let names = List.map snd (names_of_local_assums bl) in
   match na with
   | None ->
       if names = [] then error "A fixpoint needs at least one parameter." 
-      else None
+      else [], bl
   | Some (loc, id) ->
-      try Some (list_index0 (Name id) names)
-      with Not_found ->
-        user_err_loc(loc,"",
-        str "No parameter named " ++ Nameops.pr_id id ++ str".")
+      let rec aux acc = function
+	| LocalRawAssum (bls, k, t) as x :: rest ->
+	    let l, r = list_split_when (fun (loc, na) -> na = Name id) bls in
+	      if r = [] then aux (x :: acc) rest 
+	      else 
+		(List.rev (if l = [] then acc else LocalRawAssum (l, k, t) :: acc), 
+		 LocalRawAssum (r, k, t) :: rest)
+	| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
+	| [] ->
+            user_err_loc(loc,"",
+			 str "No parameter named " ++ Nameops.pr_id id ++ str".")
+      in aux [] bl
 
 (* Used in correctness and interface *)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 8f1fa5c3d4..a30c14966a 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -198,7 +198,7 @@ val coerce_reference_to_id : reference -> identifier
 val coerce_to_id : constr_expr -> identifier located
 val coerce_to_name : constr_expr -> name located
 
-val index_of_annot : local_binder list -> identifier located option -> int option
+val split_at_annot : local_binder list -> identifier located option -> local_binder list * local_binder list
 
 val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
 val prod_constr_expr : constr_expr -> local_binder list -> constr_expr