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

1 files changed, 14 insertions, 6 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 5fade008c..e9a81f09c 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 *)