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.

1 files changed, 3 insertions, 3 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index feb3bf0187..52d5c9c91e 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -188,7 +188,7 @@ let is_reversible_pattern bound depth f l =
 (* Precondition: rels in env are for inductive types only *)
 let add_free_rels_until strict strongly_strict revpat bound env m pos acc =
   let rec frec rig (env,depth as ed) c =
-    let hd = if strict then whd_betadeltaiota env c else c in
+    let hd = if strict then whd_all env c else c in
     let c = if strongly_strict then hd else c in
     match kind_of_term hd with
     | Rel n when (n < bound+depth) && (n >= depth) ->
@@ -236,7 +236,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let rigid = ref true in
   let open Context.Rel.Declaration in
   let rec aux env avoid n names t =
-    let t = whd_betadeltaiota env t in
+    let t = whd_all env t in
     match kind_of_term t with
       | Prod (na,a,b) ->
 	  let na',avoid' = find_displayed_name_in all avoid na (names,b) in
@@ -250,7 +250,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
 	    add_free_rels_until strict strongly_strict revpat n env t Conclusion v
 	  else v
   in
-  match kind_of_term (whd_betadeltaiota env t) with
+  match kind_of_term (whd_all env t) with
     | Prod (na,a,b) ->
 	let na',avoid = find_displayed_name_in all [] na ([],b) in
 	let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in