Fix part 3 of coq#18215

interp/constrexpr_ops.ml

@@ -551,46 +551,6 @@ let patntn_loc ?loc (args,argslist,binders) =
 let error_invalid_pattern_notation ?loc () =
   CErrors.user_err ?loc  (str "Invalid notation for pattern.")
 
-(* Interpret the index of a recursion order annotation *)
-let split_at_annot bl na =
-  let open CAst in
-  let names = List.map (fun { v } -> v) (names_of_local_assums bl) in
-  match na with
-  | None ->
-    begin match names with
-      | [] -> CErrors.user_err (Pp.str "A fixpoint needs at least one parameter.")
-      | _ -> ([], bl)
-    end
-  | Some { loc; v = id } ->
-    let rec aux acc = function
-      | CLocalAssum (bls, k, t) as x :: rest ->
-        let test { CAst.v = na } = match na with
-          | Name id' -> Id.equal id id'
-          | Anonymous -> false
-        in
-        let l, r = List.split_when test bls in
-        begin match r with
-          | [] -> aux (x :: acc) rest
-          | _ ->
-            let ans = match l with
-              | [] -> acc
-              | _ -> CLocalAssum (l, k, t) :: acc
-            in
-            (List.rev ans, CLocalAssum (r, k, t) :: rest)
-        end
-      | CLocalDef ({ CAst.v = na },_,_) as x :: rest ->
-        if Name.equal (Name id) na then
-          CErrors.user_err ?loc
-            (Id.print id ++ str" must be a proper parameter and not a local definition.")
-        else
-          aux (x :: acc) rest
-      | CLocalPattern _ :: rest ->
-        Loc.raise ?loc (Gramlib.Grammar.Error "pattern with quote not allowed after fix")
-      | [] ->
-        CErrors.user_err ?loc
-          (str "No parameter named " ++ Id.print id ++ str".")
-    in aux [] bl
-
 (** Pseudo-constructors *)
 
 let mkIdentC id   = CAst.make @@ CRef (qualid_of_ident id,None)

interp/constrexpr_ops.mli

@@ -124,8 +124,6 @@ val occur_var_constr_expr : Id.t -> constr_expr -> bool
 (** Return all (non-qualified) names treating binders as names *)
 val names_of_constr_expr : constr_expr -> Id.Set.t
 
-val split_at_annot : local_binder_expr list -> lident option -> local_binder_expr list * local_binder_expr list
-
 val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> notation -> (int * int) list
 val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> notation -> (int * int) list
 

test-suite/bugs/bug_18215.v

@@ -1,2 +1,5 @@
 Fail Definition a := fix f {struct unbound} :=
   fun (t : unit) => tt.
+
+Generalizable Variable A.
+Fixpoint fails `(l : list A) {struct l} : unit := tt.

vernac/comFixpoint.ml

@@ -103,17 +103,31 @@ let check_true_recursivity env evd ~isfix fixl =
     | [x,Inr []] -> warn_non_recursive (x,isfix)
     | _ -> ()
 
+(* Interpret the index of a recursion order annotation *)
+exception Found of int
+let find_rec_annot bl ctx na =
+  let name = Name na.CAst.v in
+  try
+    Context.Rel.fold_outside (fun decl n ->
+      match Context.Rel.Declaration.(get_value decl, Name.equal (get_name decl) name) with
+      | None, true -> raise (Found n)
+      | Some _, true ->
+          let loc = List.find_map (fun id -> if Name.equal name id.CAst.v then Some id.CAst.loc else None) (Constrexpr_ops.names_of_local_binders bl) in
+          let loc = Option.default na.CAst.loc loc in
+          CErrors.user_err ?loc
+            (Name.print name ++ str" must be a proper parameter and not a local definition.")
+      | None, false -> n + 1
+      | Some _, false -> n (* let-ins don't count *))
+      ~init:0 ctx |> ignore;
+    CErrors.user_err ?loc:na.loc
+      (str "No parameter named " ++ Id.print na.v ++ str".");
+  with
+    Found k -> k
+
 let interp_fix_context ~program_mode ~cofix env sigma fix =
-  let before, after =
-    if not cofix
-    then Constrexpr_ops.split_at_annot fix.Vernacexpr.binders fix.Vernacexpr.rec_order
-    else [], fix.Vernacexpr.binders in
-  let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in
-  let sigma, (impl_env', ((env'', ctx'), imps')) =
-    interp_context_evars ~program_mode ~impl_env env' sigma after
-  in
-  let annot = Option.map (fun _ -> List.length (Termops.assums_of_rel_context ctx)) fix.Vernacexpr.rec_order in
-  sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
+  let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma fix.Vernacexpr.binders in
+  let annot = Option.map (find_rec_annot fix.Vernacexpr.binders ctx) fix.Vernacexpr.rec_order in
+  sigma, ((env', ctx), (impl_env, imps), annot)
 
 let interp_fix_ccl ~program_mode sigma impls (env,_) fix =
   let flags = Pretyping.{ all_no_fail_flags with program_mode } in