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.

6 files changed, 18 insertions, 18 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 316a79482f..63b5e2a702 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -533,7 +533,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
       | Ind (i,_) -> is_class (IndRef i)
       | _ ->
           let env' = Environ.push_rel_context ctx env in
-          let ty' = whd_betadeltaiota env' ar in
+          let ty' = whd_all env' ar in
                if not (Term.eq_constr ty' ar) then iscl env' ty'
                else false
   in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 26166bd834..c3796b4842 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -62,7 +62,7 @@ let contradiction_context =
       | d :: rest ->
           let id = get_id d in
           let typ = nf_evar sigma (get_type d) in
-	  let typ = whd_betadeltaiota env sigma typ in
+	  let typ = whd_all env sigma typ in
 	  if is_empty_type typ then
 	    simplest_elim (mkVar id)
 	  else match kind_of_term typ with
@@ -84,7 +84,7 @@ let contradiction_context =
   end }
 
 let is_negation_of env sigma typ t =
-  match kind_of_term (whd_betadeltaiota env sigma t) with
+  match kind_of_term (whd_all env sigma t) with
     | Prod (na,t,u) ->
       let u = nf_evar sigma u in
       is_empty_type u && is_conv_leq env sigma typ t
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 35be1fcb6e..1950356b38 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -720,8 +720,8 @@ let find_positions env sigma t1 t2 =
     then [(List.rev posn,t1,t2)] else []
   in
   let rec findrec sorts posn t1 t2 =
-    let hd1,args1 = whd_betadeltaiota_stack env sigma t1 in
-    let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in
+    let hd1,args1 = whd_all_stack env sigma t1 in
+    let hd2,args2 = whd_all_stack env sigma t2 in
     match (kind_of_term hd1, kind_of_term hd2) with
       | Construct (sp1,_), Construct (sp2,_)
           when Int.equal (List.length args1) (constructor_nallargs_env env sp1)
@@ -1283,7 +1283,7 @@ let build_injector env sigma dflt c cpath =
 
 (*
 let try_delta_expand env sigma t =
-  let whdt = whd_betadeltaiota env sigma t  in
+  let whdt = whd_all env sigma t  in
   let rec hd_rec c  =
     match kind_of_term c with
       | Construct _ -> whdt
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 4c2c84d23b..f2c72c2f3d 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -464,7 +464,7 @@ let match_eq_nf gls eqn (ref, hetero) =
   match Id.Map.bindings (pf_matches gls pat eqn) with
     | [(m1,t);(m2,x);(m3,y)] ->
         assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
-	(t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y)
+	(t,pf_whd_all gls x,pf_whd_all gls y)
     | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms")
 
 let dest_nf_eq gls eqn =
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 70782ec648..63b1a7b541 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -114,7 +114,7 @@ let max_prefix_sign lid sign =
     | id::l -> snd (max_rec (id, sign_prefix id sign) l)
 *)
 let rec add_prods_sign env sigma t =
-  match kind_of_term (whd_betadeltaiota env sigma t) with
+  match kind_of_term (whd_all env sigma t) with
     | Prod (na,c1,b) ->
 	let id = id_of_name_using_hdchar env t na in
 	let b'= subst1 (mkVar id) b in
@@ -167,7 +167,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       let goal = mkArrow i (applist(mkVar p, List.rev revargs)) in
       (pty,goal)
   in
-  let npty = nf_betadeltaiota env sigma pty in
+  let npty = nf_all env sigma pty in
   let extenv = push_named (LocalAssum (p,npty)) env in
   extenv, goal
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cf842d6f19..9a39773a84 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -537,7 +537,7 @@ let fix ido n = match ido with
     mutual_fix id n [] 0
 
 let rec check_is_mutcoind env sigma cl =
-  let b = whd_betadeltaiota env sigma cl in
+  let b = whd_all env sigma cl in
   match kind_of_term b with
   | Prod (na, c1, b) ->
     let open Context.Rel.Declaration in
@@ -774,15 +774,15 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
     let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in
     if not b then
       if
-        isSort (whd_betadeltaiota env sigma t1) &&
-        isSort (whd_betadeltaiota env sigma t2)
+        isSort (whd_all env sigma t1) &&
+        isSort (whd_all env sigma t2)
       then (mayneedglobalcheck := true; sigma)
       else
         errorlabstrm "convert-check-hyp" (str "Types are incompatible.")
     else sigma
   end
   else
-    if not (isSort (whd_betadeltaiota env sigma t1)) then
+    if not (isSort (whd_all env sigma t1)) then
       errorlabstrm "convert-check-hyp" (str "Not a type.")
     else sigma
 
@@ -1204,7 +1204,7 @@ let cut c =
       try
         (** Backward compat: ensure that [c] is well-typed. *)
         let typ = Typing.unsafe_type_of env sigma c in
-        let typ = whd_betadeltaiota env sigma typ in
+        let typ = whd_all env sigma typ in
         match kind_of_term typ with
         | Sort _ -> true
         | _ -> false
@@ -2293,8 +2293,8 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
-    let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in
-    let t = whd_betadeltaiota (type_of (mkVar id)) in
+    let whd_all = Tacmach.New.pf_apply whd_all gl in
+    let t = whd_all (type_of (mkVar id)) in
     let eqtac, thin = match match_with_equality_type t with
     | Some (hdcncl,[_;lhs;rhs]) ->
         if l2r && isVar lhs && not (occur_var env (destVar lhs) rhs) then
@@ -4253,7 +4253,7 @@ let check_enough_applied env sigma elim =
   | None ->
       (* No eliminator given *)
       fun u ->
-      let t,_ = decompose_app (whd_betadeltaiota env sigma u) in isInd t
+      let t,_ = decompose_app (whd_all env sigma u) in isInd t
   | Some elimc ->
       let elimt = Retyping.get_type_of env sigma (fst elimc) in
       let scheme = compute_elim_sig ~elimc elimt in
@@ -4573,7 +4573,7 @@ let maybe_betadeltaiota_concl allowred gl =
   if not allowred then concl
   else
     let env = Proofview.Goal.env gl in
-    whd_betadeltaiota env sigma concl
+    whd_all env sigma concl
 
 let reflexivity_red allowred =
   Proofview.Goal.enter { enter = begin fun gl ->