diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-22 17:38:18 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 08:58:19 +0100 |
| commit | f22ad605a14eb14d11b0a1615f7014f2dca3b483 (patch) | |
| tree | dd5e6675dcc46209f1ac33dad40292e85450ff1f | |
| parent | f4002e6c85f575fc8451adb80dba705795f0a0c9 (diff) | |
An example in centralizing similar functions to a common place so that
cleaning the interfaces is eventually easier. Here, adding
find_mrectype_vect to simplify vnorm.ml.
| -rw-r--r-- | pretyping/inductiveops.ml | 7 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 1 | ||||
| -rw-r--r-- | pretyping/vnorm.ml | 8 |
3 files changed, 7 insertions, 9 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index cb091f2d6..632e00ed7 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -430,12 +430,15 @@ let extract_mrectype t = | Ind ind -> (ind, l) | _ -> raise Not_found -let find_mrectype env sigma c = - let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in +let find_mrectype_vect env sigma c = + let (t, l) = decompose_appvect (whd_betadeltaiota env sigma c) in match kind_of_term t with | Ind ind -> (ind, l) | _ -> raise Not_found +let find_mrectype env sigma c = + let (ind, v) = find_mrectype_vect env sigma c in (ind, Array.to_list v) + let find_rectype env sigma c = let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in match kind_of_term t with diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 757599a3c..9036f521e 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -159,6 +159,7 @@ val build_branch_type : env -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) val extract_mrectype : constr -> pinductive * constr list val find_mrectype : env -> evar_map -> types -> pinductive * constr list +val find_mrectype_vect : env -> evar_map -> types -> pinductive * constr array val find_rectype : env -> evar_map -> types -> inductive_type val find_inductive : env -> evar_map -> types -> pinductive * constr list val find_coinductive : env -> evar_map -> types -> pinductive * constr list diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index be772a667..60140a31d 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -45,13 +45,7 @@ let invert_tag cst tag reloc_tbl = with Find_at j -> (j+1) (* Argggg, ces constructeurs de ... qui commencent a 1*) -let find_rectype_a env c = - let (t, l) = - let t = whd_betadeltaiota env c in - try destApp t with DestKO -> (t,[||]) in - match kind_of_term t with - | Ind ind -> (ind, l) - | _ -> raise Not_found +let find_rectype_a env c = Inductiveops.find_mrectype_vect env Evd.empty c (* Instantiate inductives and parameters in constructor type *) |