Merge branch 'reduction-flags' into trunk

Was PR#231: Separate flags for fix/cofix/match reduction and clean reduction
function names, itself a revision of PR#117: Isolating flags for cofix/fix
reduction + adjusting names of reduction functions to what they do

1 files changed, 16 insertions, 16 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 8e26370ec..29966facb 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -29,20 +29,20 @@ let lookup_mind_specif env (kn,tyi) =
   (mib, mib.mind_packets.(tyi))
 
 let find_rectype env c =
-  let (t, l) = decompose_app (whd_betadeltaiota env c) in
+  let (t, l) = decompose_app (whd_all env c) in
   match kind_of_term t with
   | Ind ind -> (ind, l)
   | _ -> raise Not_found
 
 let find_inductive env c =
-  let (t, l) = decompose_app (whd_betadeltaiota env c) in
+  let (t, l) = decompose_app (whd_all env c) in
   match kind_of_term t with
     | Ind ind
         when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l)
     | _ -> raise Not_found
 
 let find_coinductive env c =
-  let (t, l) = decompose_app (whd_betadeltaiota env c) in
+  let (t, l) = decompose_app (whd_all env c) in
   match kind_of_term t with
     | Ind ind
         when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l)
@@ -313,7 +313,7 @@ let check_allowed_sort ksort specif =
 let is_correct_arity env c pj ind specif params =
   let arsign,_ = get_instantiated_arity ind specif params in
   let rec srec env pt ar =
-    let pt' = whd_betadeltaiota env pt in
+    let pt' = whd_all env pt in
     match kind_of_term pt', ar with
       | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
           let () =
@@ -323,7 +323,7 @@ let is_correct_arity env c pj ind specif params =
       (* The last Prod domain is the type of the scrutinee *)
       | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
 	 let env' = push_rel (LocalAssum (na1,a1)) env in
-	 let ksort = match kind_of_term (whd_betadeltaiota env' a2) with
+	 let ksort = match kind_of_term (whd_all env' a2) with
 	 | Sort s -> family_of_sort s
 	 | _ -> raise (LocalArity None) in
 	 let dep_ind = build_dependent_inductive ind specif params in
@@ -563,7 +563,7 @@ let check_inductive_codomain env p =
   let env = push_rel_context absctx env in
   let arctx, s = dest_prod_assum env ar in
   let env = push_rel_context arctx env in
-  let i,l' = decompose_app (whd_betadeltaiota env s) in
+  let i,l' = decompose_app (whd_all env s) in
   isInd i
 
 (* The following functions are almost duplicated from indtypes.ml, except
@@ -586,7 +586,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
 
 let rec ienv_decompose_prod (env,_ as ienv) n c =
  if Int.equal n 0 then (ienv,c) else
-   let c' = whd_betadeltaiota env c in
+   let c' = whd_all env c in
    match kind_of_term c' with
    Prod(na,a,b) ->
      let ienv' = ienv_push_var ienv (na,a,mk_norec) in
@@ -618,7 +618,7 @@ close to check_positive in indtypes.ml, but does no positivity check and does no
 compute the number of recursive arguments. *)
 let get_recargs_approx env tree ind args =
   let rec build_recargs (env, ra_env as ienv) tree c =
-    let x,largs = decompose_app (whd_betadeltaiota env c) in
+    let x,largs = decompose_app (whd_all env c) in
     match kind_of_term x with
     | Prod (na,b,d) ->
        assert (List.is_empty largs);
@@ -677,7 +677,7 @@ let get_recargs_approx env tree ind args =
 
   and build_recargs_constructors ienv trees c =
     let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c =
-      let x,largs = decompose_app (whd_betadeltaiota env c) in
+      let x,largs = decompose_app (whd_all env c) in
 	match kind_of_term x with
 
           | Prod (na,b,d) ->
@@ -706,7 +706,7 @@ let restrict_spec env spec p =
   let env = push_rel_context absctx env in
   let arctx, s = dest_prod_assum env ar in
   let env = push_rel_context arctx env in
-  let i,args = decompose_app (whd_betadeltaiota env s) in
+  let i,args = decompose_app (whd_all env s) in
   match kind_of_term i with
   | Ind i ->
      begin match spec with
@@ -727,7 +727,7 @@ let restrict_spec env spec p =
 
 let rec subterm_specif renv stack t =
   (* maybe reduction is not always necessary! *)
-  let f,l = decompose_app (whd_betadeltaiota renv.env t) in
+  let f,l = decompose_app (whd_all renv.env t) in
     match kind_of_term f with
     | Rel k -> subterm_var k renv
     | Case (ci,p,c,lbr) ->
@@ -854,11 +854,11 @@ let filter_stack_domain env ci p stack =
   if noccur_with_meta 1 (Context.Rel.length absctx) ar then stack
   else let env = push_rel_context absctx env in
   let rec filter_stack env ar stack =
-    let t = whd_betadeltaiota env ar in
+    let t = whd_all env ar in
     match stack, kind_of_term t with
     | elt :: stack', Prod (n,a,c0) ->
       let d = LocalAssum (n,a) in
-      let ty, args = decompose_app (whd_betadeltaiota env a) in
+      let ty, args = decompose_app (whd_all env a) in
       let elt = match kind_of_term ty with
       | Ind ind -> 
         let spec' = stack_element_specif elt in
@@ -1047,7 +1047,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
     (* check fi does not appear in the k+1 first abstractions,
        gives the type of the k+1-eme abstraction (must be an inductive)  *)
     let rec check_occur env n def =
-      match kind_of_term (whd_betadeltaiota env def) with
+      match kind_of_term (whd_all env def) with
         | Lambda (x,a,b) ->
 	    if noccur_with_meta n nbfix a then
 	      let env' = push_rel (LocalAssum (x,a)) env in
@@ -1101,7 +1101,7 @@ let anomaly_ill_typed () =
   anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor")
 
 let rec codomain_is_coind env c =
-  let b = whd_betadeltaiota env c in
+  let b = whd_all env c in
   match kind_of_term b with
     | Prod (x,a,b) ->
 	codomain_is_coind (push_rel (LocalAssum (x,a)) env) b
@@ -1113,7 +1113,7 @@ let rec codomain_is_coind env c =
 let check_one_cofix env nbfix def deftype =
   let rec check_rec_call env alreadygrd n tree vlra  t =
     if not (noccur_with_meta n nbfix t) then
-      let c,args = decompose_app (whd_betadeltaiota env t) in
+      let c,args = decompose_app (whd_all env t) in
       match kind_of_term c with
 	| Rel p when  n <= p && p < n+nbfix ->
 	    (* recursive call: must be guarded and no nested recursive