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/glob_term_to_relation.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/glob_term_to_relation.ml')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 11e4fa0ac7..6ed61043f9 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -568,6 +568,7 @@ let rec build_entry_lc env sigma funnames avoid rt : | GProd _ -> user_err Pp.(str "Cannot apply a type") | GInt _ -> user_err Pp.(str "Cannot apply an integer") | GFloat _ -> user_err Pp.(str "Cannot apply a float") + | GArray _ -> user_err Pp.(str "Cannot apply an array") (* end of the application treatement *) ) | GLambda (n, _, t, b) -> (* we first compute the list of constructor @@ -672,6 +673,7 @@ let rec build_entry_lc env sigma funnames avoid rt : build_entry_lc env sigma funnames avoid match_expr | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast (b, _) -> build_entry_lc env sigma funnames avoid b + | GArray _ -> user_err Pp.(str "Not handled GArray") and build_entry_lc_from_case env sigma funname make_discr (el : tomatch_tuples) (brl : Glob_term.cases_clauses) avoid : glob_constr build_entry_return = @@ -1196,7 +1198,7 @@ let rec compute_cst_params relnames params gt = discrimination ones *) | GSort _ -> params | GHole _ -> params - | GIf _ | GRec _ | GCast _ -> + | GIf _ | GRec _ | GCast _ | GArray _ -> CErrors.user_err ~hdr:"compute_cst_params" (str "Not handled case")) gt |