diff options
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_11816.v | 2 |
2 files changed, 4 insertions, 2 deletions
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 diff --git a/test-suite/bugs/closed/bug_11816.v b/test-suite/bugs/closed/bug_11816.v new file mode 100644 index 0000000000..82a317b250 --- /dev/null +++ b/test-suite/bugs/closed/bug_11816.v @@ -0,0 +1,2 @@ +(* This should be an error, not an anomaly *) +Fail Definition foo := fix foo (n : nat) { wf n n } := 0. |