diff options
| author | Maxime Dénès | 2020-02-03 18:19:42 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2020-07-06 11:22:43 +0200 |
| commit | 0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6 (patch) | |
| tree | fbad060c3c2e29e81751dea414c898b5cb0fa22d /plugins/funind/recdef.ml | |
| parent | cf388fdb679adb88a7e8b3122f65377552d2fb94 (diff) | |
Primitive persistent arrays
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 701ea56c2a..64f62ba1fb 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -305,9 +305,11 @@ let check_not_nested env sigma forbidden e = | Lambda (_, t, b) -> check_not_nested t; check_not_nested b | LetIn (_, v, t, b) -> check_not_nested t; check_not_nested b; check_not_nested v - | App (f, l) -> - check_not_nested f; - Array.iter check_not_nested l + | App (f, l) -> check_not_nested f + | Array (_u, t, def, ty) -> + Array.iter check_not_nested t; + check_not_nested def; + check_not_nested ty | Proj (p, c) -> check_not_nested c | Const _ -> () | Ind _ -> () @@ -447,6 +449,7 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g = match EConstr.kind sigma expr_info.info with | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint") + | Array _ -> user_err Pp.(str "Function cannot treat arrays") | Proj _ -> user_err Pp.(str "Function cannot treat projections") | LetIn (na, b, t, e) -> let new_continuation_tac = |