From d0ed43b5cc0c31b5f0532753587f641716246bb7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 14 Nov 2020 21:29:52 +0100
Subject: Fixes #11816: using {wf ...} in a local fixpoint is an error, not an
 anomaly.

---
 interp/constrintern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 06cf19b4f7..378617af04 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1972,9 +1972,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         let env = restart_lambda_binders env in
         let idl_temp = Array.map
             (fun (id,recarg,bl,ty,_) ->
-               let recarg = Option.map (function { CAst.v = v } -> match v with
+               let recarg = Option.map (function { CAst.v = v; loc } -> match v with
                  | CStructRec i -> i
-                 | _ -> anomaly Pp.(str "Non-structural recursive argument in non-program fixpoint")) recarg
+                 | _ -> user_err ?loc Pp.(str "Well-founded induction requires Program Fixpoint or Function.")) recarg
                in
                let before, after = split_at_annot bl recarg in
                let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
-- 
cgit v1.2.3