Merge PR #18190: Support for weak cbv

Reviewed-by: SkySkimmer Ack-by: jfehrle Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
coq · Nov 21, 2023 · 7cf5e39 · 7cf5e39
2 parents 0c40866 + 82a9037
commit 7cf5e39
Show file tree

Hide file tree

Showing 16 changed files with 176 additions and 108 deletions.
diff --git a/dev/ci/user-overlays/18190-herbelin-master+weak-cbv.sh b/dev/ci/user-overlays/18190-herbelin-master+weak-cbv.sh
@@ -0,0 +1,2 @@
+overlay elpi https://github.com/herbelin/coq-elpi coq-master+adapt-coq-pr18190-whd-cbv 18190 master+weak-cbv
+overlay equations https://github.com/herbelin/Coq-Equations master+adapt-coq-pr18190-whd-cbv 18190 master+weak-cbv
diff --git a/doc/changelog/04-tactics/17503-redexpr.rst b/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).
diff --git a/doc/sphinx/proofs/writing-proofs/equality.rst b/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`

diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
@@ -506,9 +506,9 @@ reductions: [
 ]
 
 reduction: [
+| "head"
 | "beta"
 | "delta" OPT delta_reductions
-| "head"
 | "match"
 | "fix"
 | "cofix"

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
@@ -999,7 +999,7 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num
         match body.Declarations.const_body with
         | Def body ->
           let sigma = Evd.from_env env in
-          Tacred.cbv_norm_flags
+          Tacred.cbv_norm_flags ~strong:true
             (RedFlags.mkflags [RedFlags.fZETA])
             env sigma (EConstr.of_constr body)
         | Undef _ | Primitive _ | OpaqueDef _ -> user_err Pp.(str "Cannot define a principle over an axiom ")

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
@@ -1223,7 +1223,7 @@ let get_funs_constant mp =
       match body.Declarations.const_body with
       | Def body ->
         let body =
-          Tacred.cbv_norm_flags
+          Tacred.cbv_norm_flags ~strong:true
             (RedFlags.mkflags [RedFlags.fZETA])
             env
             (Evd.from_env env)