diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-22 17:11:39 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 10:07:41 +0100 |
| commit | e8c47b652a0b53f8d3f7eaa877e81910c8de55d0 (patch) | |
| tree | 85e00c1bf5d9334a4381c38e950bd71ae5ecb7e6 /pretyping/typing.ml | |
| parent | e3cefca41b568b1e517313051a111b0416cd2594 (diff) | |
Unifying betazeta_applist and prod_applist into a clearer interface.
- prod_applist
- prod_applist_assum
- lambda_applist
- lambda_applist_assum
expect an instance matching the quantified context. They are now in
term.ml, with "list" being possibly "vect".
Names are a bit arbitrary. Better propositions are welcome. They are
put in term.ml in that reduction is after all not needed, because the
intent is not to do β or ι on the fly but rather to substitute a λΓ.c
or ∀Γ.c (seen as internalization of a Γ⊢c) into one step,
independently of the idea of reducing.
On the other side:
- beta_applist
- beta_appvect
are seen as optimizations of application doing reduction on the fly
only if possible. They are then kept as functions relevant for
reduction.ml.
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index fb5927dbf..15abfefb1 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -112,8 +112,7 @@ let e_type_case_branches env evdref (ind,largs) pj c = let univ = e_is_correct_arity env evdref c pj ind specif params in let lc = build_branches_type ind specif params p in let n = (snd specif).Declarations.mind_nrealargs in - let ty = - whd_betaiota !evdref (Reduction.betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))) in + let ty = whd_betaiota !evdref (lambda_applist_assum (n+1) p (realargs@[c])) in (lc, ty, univ) let e_judge_of_case env evdref ci pj cj lfj = |