diff options
| author | Hugo Herbelin | 2020-11-14 21:29:52 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-15 14:33:11 +0100 |
| commit | d0ed43b5cc0c31b5f0532753587f641716246bb7 (patch) | |
| tree | e9a18b775551839e83d74c6f450972e0a2a74b46 | |
| parent | a118b906b3da7cb2e03a72f7a8079a7fc99c6f84 (diff) | |
Fixes #11816: using {wf ...} in a local fixpoint is an error, not an anomaly.
| -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. |