Separate flags for fix/cofix/match reduction and clean reduction function names.

This is a reimplementation of Hugo's PR#117.

We are trying to address the problem that the name of some reduction functions
was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in
reduction). Like PR#117, we are careful that no function changed semantics
without changing the names. Porting existing ML code should be a matter of
renamings a few function calls.

Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX
collectively denominated iota.

We renamed the following functions:

Closure.betadeltaiota -> Closure.all
Closure.betadeltaiotanolet -> Closure.allnolet
Reductionops.beta -> Closure.beta
Reductionops.zeta -> Closure.zeta
Reductionops.betaiota -> Closure.betaiota
Reductionops.betaiotazeta -> Closure.betaiotazeta
Reductionops.delta -> Closure.delta
Reductionops.betalet -> Closure.betazeta
Reductionops.betadelta -> Closure.betadeltazeta
Reductionops.betadeltaiota -> Closure.all
Reductionops.betadeltaiotanolet -> Closure.allnolet
Closure.no_red -> Closure.nored
Reductionops.nored -> Closure.nored
Reductionops.nf_betadeltaiota -> Reductionops.nf_all
Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta
Reductionops.whd_betadeltaiota -> Reductionops.whd_all
Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet
Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack
Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack
Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack
Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state
Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state
Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state
Reductionops.whd_eta -> Reductionops.shrink_eta
Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all
Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all

And removed the following ones:

Reductionops.whd_betaetalet
Reductionops.whd_betaetalet_stack
Reductionops.whd_betaetalet_state
Reductionops.whd_betadeltaeta_stack
Reductionops.whd_betadeltaeta_state
Reductionops.whd_betadeltaeta
Reductionops.whd_betadeltaiotaeta_stack
Reductionops.whd_betadeltaiotaeta_state
Reductionops.whd_betadeltaiotaeta

They were unused and having some reduction functions perform eta is confusing
as whd_all and nf_all don't do it.

9 files changed, 15 insertions, 15 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index bd788a425..de64368e2 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -42,7 +42,7 @@ let whd env=
     (fun t -> Closure.whd_val infos (Closure.inject t))
 
 let whd_delta env=
-   let infos=Closure.create_clos_infos Closure.betadeltaiota env in
+   let infos=Closure.create_clos_infos Closure.all env in
     (fun t -> Closure.whd_val infos (Closure.inject t))
 
 (* decompose member of equality in an applicative format *)
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 34307a358..c0ef34305 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -153,7 +153,7 @@ let interp_constr check_sort env sigma c =
     fst (understand env sigma (fst c))
 
 let special_whd env =
-  let infos=Closure.create_clos_infos Closure.betadeltaiota env in
+  let infos=Closure.create_clos_infos Closure.all env in
     (fun t -> Closure.whd_val infos (Closure.inject t))
 
 let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq))
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 836f1982d..b6c34d270 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -84,7 +84,7 @@ let tcl_erase_info gls =
   tcl_change_info_gen info_gen gls
 
 let special_whd gl=
-  let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in
+  let infos=Closure.create_clos_infos Closure.all (pf_env gl) in
     (fun t -> Closure.whd_val infos (Closure.inject t))
 
 let special_nf gl=
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 0153348de..4308b4633 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -74,7 +74,7 @@ type flag = info * scheme
   Really important function. *)
 
 let rec flag_of_type env t : flag =
-  let t = whd_betadeltaiota env none t in
+  let t = whd_all env none t in
   match kind_of_term t with
     | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c
     | Sort s when Sorts.is_prop s -> (Logic,TypeScheme)
@@ -102,14 +102,14 @@ let is_info_scheme env t = match flag_of_type env t with
 (*s [type_sign] gernerates a signature aimed at treating a type application. *)
 
 let rec type_sign env c =
-  match kind_of_term (whd_betadeltaiota env none c) with
+  match kind_of_term (whd_all env none c) with
     | Prod (n,t,d) ->
 	(if is_info_scheme env t then Keep else Kill Kprop)
 	:: (type_sign (push_rel_assum (n,t) env) d)
     | _ -> []
 
 let rec type_scheme_nb_args env c =
-  match kind_of_term (whd_betadeltaiota env none c) with
+  match kind_of_term (whd_all env none c) with
     | Prod (n,t,d) ->
 	let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in
 	if is_info_scheme env t then n+1 else n
@@ -135,7 +135,7 @@ let make_typvar n vl =
   next_ident_away id' vl
 
 let rec type_sign_vl env c =
-  match kind_of_term (whd_betadeltaiota env none c) with
+  match kind_of_term (whd_all env none c) with
     | Prod (n,t,d) ->
 	let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in
 	if not (is_info_scheme env t) then Kill Kprop::s, vl
@@ -143,7 +143,7 @@ let rec type_sign_vl env c =
     | _ -> [],[]
 
 let rec nb_default_params env c =
-  match kind_of_term (whd_betadeltaiota env none c) with
+  match kind_of_term (whd_all env none c) with
     | Prod (n,t,d) ->
 	let n = nb_default_params (push_rel_assum (n,t) env) d in
 	if is_default env t then n+1 else n
@@ -489,7 +489,7 @@ and extract_really_ind env kn mib =
 *)
 
 and extract_type_cons env db dbmap c i =
-  match kind_of_term (whd_betadeltaiota env none c) with
+  match kind_of_term (whd_all env none c) with
     | Prod (n,t,d) ->
 	let env' = push_rel_assum (n,t) env in
 	let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 81dfa603d..3a9ecc9ff 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -441,7 +441,7 @@ let error_MPfile_as_mod mp b =
 let argnames_of_global r =
   let typ = Global.type_of_global_unsafe r in
   let rels,_ =
-    decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in
+    decompose_prod (Reduction.whd_all (Global.env ()) typ) in
   List.rev_map fst rels
 
 let msg_of_implicit = function
@@ -880,7 +880,7 @@ let extract_constant_inline inline r ids s =
     | ConstRef kn ->
 	let env = Global.env () in
 	let typ = Global.type_of_global_unsafe (ConstRef kn) in
-	let typ = Reduction.whd_betadeltaiota env typ in
+	let typ = Reduction.whd_all env typ in
 	if Reduction.is_arity env typ
 	  then begin
 	    let nargs = Hook.get use_type_scheme_nb_args env typ in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 5eff2f277..1394f4764 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -107,7 +107,7 @@ let mk_open_instance id idc gl m t=
       let typ=pf_unsafe_type_of gl idc in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
-      let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
+      let (nam,_,_)=destProd (whd_all env evmap typ) in
 	match nam with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 52094cf08..146749d32 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -281,7 +281,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
 	  List.fold_left2 compute_substitution sub args1 args2
 	end
       else
-	if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_betadeltaiota env t1) t2)  "cannot solve (diff)"
+	if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_all env t1) t2)  "cannot solve (diff)"
     in
     let sub = compute_substitution Int.Map.empty (snd t1) (snd t2) in
     let sub = compute_substitution sub (fst t1) (fst t2) in
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 0a0b45915..bb9266db1 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -67,7 +67,7 @@ let l_D_Or = lazy (constant "D_Or")
 
 
 let special_whd gl=
-  let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in
+  let infos=Closure.create_clos_infos Closure.all (pf_env gl) in
     (fun t -> Closure.whd_val infos (Closure.inject t))
 
 let special_nf gl=
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 55241ab2b..a6744916a 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -82,7 +82,7 @@ let lookup_map map =
     errorlabstrm"lookup_map"(str"map "++qs map++str"not found")
 
 let protect_red map env sigma c =
-  kl (create_clos_infos betadeltaiota env)
+  kl (create_clos_infos all env)
     (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);;
 
 let protect_tac map =