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 /pretyping/vnorm.ml | |
| 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.
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 8 |
1 files changed, 1 insertions, 7 deletions
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 *) |