From e8c47b652a0b53f8d3f7eaa877e81910c8de55d0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 22 Nov 2015 17:11:39 +0100
Subject: 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.
---
 pretyping/inductiveops.ml | 2 +-
 pretyping/typing.ml       | 3 +--
 2 files changed, 2 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index cc4ea5a4a2..82168f9c4a 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -518,7 +518,7 @@ let type_case_branches_with_names env indspec p c =
   let (params,realargs) = List.chop nparams args in
   let lbrty = Inductive.build_branches_type ind specif params p in
   (* Build case type *)
-  let conclty = Reduction.betazeta_appvect (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in
+  let conclty = lambda_appvect_assum (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in
   (* Adjust names *)
   if is_elim_predicate_explicitly_dependent env p (ind,params) then
     (set_pattern_names env (fst ind) lbrty, conclty)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index fb5927dbf7..15abfefb15 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 =
-- 
cgit v1.2.3