Binding weak cbv to reduction tactic "cbv head".

Include some rephrasing in doc, co-authored by Jim.

Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>

doc/changelog/04-tactics/17503-redexpr.rst

@@ -1,6 +1,7 @@
 - **Added:**
-  :tacn:`lazy`, :tacn:`simpl` and :tacn:`cbn` and the associated :cmd:`Eval` and :tacn:`eval` reductions
-  learnt to do head reduction when given flag `head`
+  :tacn:`lazy`, :tacn:`simpl`, :tacn:`cbn` and :tacn:`cbv` and the associated :cmd:`Eval`
+  and :tacn:`eval` reductions learned to do head reduction when given flag `head`
   (eg `Eval lazy head in (fun x => Some ((fun y => y) x)) 0` produces `Some ((fun y => y) 0)`)
   (`#17503 <https://github.com/coq/coq/pull/17503>`_,
-  by Gaëtan Gilbert).
+  by Gaëtan Gilbert; :tacn:`cbv` case added in `#18190 <https://github.com/coq/coq/pull/18190>`_,
+  by Hugo Herbelin).

doc/sphinx/proofs/writing-proofs/equality.rst

@@ -493,9 +493,9 @@ which reduction engine to use.  See :ref:`type-cast`.)  For example:
    .. prodn::
       reductions ::= {+ @reduction }
       | {? head } @delta_reductions
-      reduction ::= beta
+      reduction ::= head
+      | beta
       | delta {? @delta_reductions }
-      | head
       | match
       | fix
       | cofix
@@ -508,8 +508,8 @@ which reduction engine to use.  See :ref:`type-cast`.)  For example:
    then only the named reductions are applied.  The reductions include:
 
    `head`
-     Do only head reduction, without going under binders.  Only
-     supported by :tacn:`simpl`, :tacn:`cbn` and :tacn:`lazy`.
+     Do only head reduction, without going under binders.
+     Supported by :tacn:`simpl`, :tacn:`cbv`, :tacn:`cbn` and :tacn:`lazy`.
      If this is the only specified reduction, all other reductions are applied.
 
    `beta`

doc/tools/docgram/orderedGrammar

@@ -499,9 +499,9 @@ reductions: [
 ]
 
 reduction: [
+| "head"
 | "beta"
 | "delta" OPT delta_reductions
-| "head"
 | "match"
 | "fix"
 | "cofix"

tactics/redexpr.ml

@@ -253,7 +253,7 @@ let reduction_of_red_expr_val = function
     in
      (contextualize am o,DEFAULTcast)
   | Cbv (Norm, f) -> (e_red (cbv_norm_flags ~strong:true f),DEFAULTcast)
-  | Cbv (Head, _) -> CErrors.user_err Pp.(str "cbv does not support head-only reduction.")
+  | Cbv (Head, f) -> (e_red (cbv_norm_flags ~strong:false f),DEFAULTcast)
   | Cbn (w,f) ->
     let cbn = match w with Norm -> Cbn.norm_cbn | Head -> Cbn.whd_cbn in
      (e_red (cbn f), DEFAULTcast)

test-suite/output/reduction.out

@@ -13,6 +13,8 @@
              | S p => S (add p m)
              end) 1 2)
      : nat
+     = 4
+     : nat
      = (fix add (n m : nat) {struct n} : nat :=
           match n with
           | 0 => m
@@ -23,6 +25,10 @@
      : nat
      = S (1 + 2 + 2)
      : nat
+     = 6
+     : nat
+     = ignore (fun x : nat => 1 + x)
+     : unit
      = ignore (fun x : nat => 1 + x)
      : unit
      = ignore (fun x : nat => 1 + x)

test-suite/output/reduction.v

@@ -14,14 +14,18 @@ Eval hnf in match (plus (S n) O) with S n => n | _ => O end.
 Eval simpl head in 2 + 2.
 Eval cbn head in 2 + 2.
 Eval lazy head in 2 + 2.
+Eval cbv head in 2 + 2.
 
 Eval lazy head delta in 2 + 2.
 
 Eval simpl head in 2 + (2 + 2).
 
 Eval simpl head in (2 + 2) + 2.
 
+Eval cbv head in (2 + 2) + 2.
+
 Axiom ignore : forall {T}, T -> unit.
 Eval simpl head in ignore (fun x => 1 + x).
 Eval cbn head in ignore (fun x => 1 + x).
 Eval lazy head in ignore (fun x => 1 + x).
+Eval cbv head in ignore (fun x => 1 + x).