Merge PR #13232: Adding an if-then-else syntax to Ltac2.

Reviewed-by: MSoegtropIMC
Ack-by: Zimmi48
Reviewed-by: jfehrle

5 files changed, 18 insertions, 6 deletions

diff --git a/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst b/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst
new file mode 100644
index 0000000000..d105561a23
--- /dev/null
+++ b/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  An if-then-else syntax to Ltac2
+  (`#13232 <https://github.com/coq/coq/pull/13232>`_,
+  fixes `#10110 <https://github.com/coq/coq/issues/10110>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 64fc1133f0..41f376c43d 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -38,7 +38,6 @@ Current limitations include:
   - Printing functions are limited and awkward to use.  Only a few data types are
     printable.
   - Deep pattern matching and matching on tuples don't work.
-  - If statements on Ltac2 boolean values
   - A convenient way to build terms with casts through the low-level API. Because the
     cast type is opaque, building terms with casts currently requires an awkward construction like the
     following, which also incurs extra overhead to repeat typechecking for each
@@ -345,12 +344,10 @@ Ltac2 Definitions
 
       .. coqtop:: all
 
-         Ltac2 mutable rec f b := match b with true => 0 | _ => f true end.
-         Ltac2 Set f := fun b =>
-                  match b with true => 1 | _ => f true end.
+         Ltac2 mutable rec f b := if b then 0 else f true.
+         Ltac2 Set f := fun b => if b then 1 else f true.
          Ltac2 Eval (f false).
-         Ltac2 Set f as oldf := fun b =>
-                  match b with true => 2 | _ => oldf false end.
+         Ltac2 Set f as oldf := fun b => if b then  2 else oldf false.
          Ltac2 Eval (f false).
 
       In the definition, the `f` in the body is resolved statically
@@ -1149,6 +1146,13 @@ Match on values
       | @tac2pat1 , {*, @tac2pat1 }
       | @tac2pat1
 
+.. tacn:: if @ltac2_expr5__test then @ltac2_expr5__then else @ltac2_expr5__else
+   :name: if-then-else (Ltac2)
+
+   Equivalent to a :tacn:`match <match (Ltac2)>` on a boolean value.  If the
+   :n:`@ltac2_expr5__test` evaluates to true, :n:`@ltac2_expr5__then`
+   is evaluated.  Otherwise :n:`@ltac2_expr5__else` is evaluated.
+
 .. note::
 
    For now, deep pattern matching is not implemented.
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index f6a684bbd7..a143a6c7cf 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -2198,6 +2198,7 @@ ltac2_expr5: [
 | REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" ltac2_expr6      (* Ltac2 plugin *)
 | WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr6 TAG Ltac2
 | MOVETO simple_tactic "match" ltac2_expr5 "with" OPT ltac2_branches "end"      (* Ltac2 plugin *)
+| MOVETO simple_tactic "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5      (* Ltac2 plugin *)
 | DELETE simple_tactic
 ]
 
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index c764cb6f37..0638e1753b 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -2586,6 +2586,7 @@ ltac2_expr5: [
 | "fun" LIST1 G_LTAC2_input_fun "=>" ltac2_expr6      (* Ltac2 plugin *)
 | "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" ltac2_expr6      (* Ltac2 plugin *)
 | "match" ltac2_expr5 "with" G_LTAC2_branches "end"      (* Ltac2 plugin *)
+| "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5      (* Ltac2 plugin *)
 | ltac2_expr4      (* Ltac2 plugin *)
 ]
 
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 12a7bc684d..7d773e3a5b 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1640,6 +1640,7 @@ simple_tactic: [
 | "ring" OPT ( "[" LIST1 one_term "]" )
 | "ring_simplify" OPT ( "[" LIST1 one_term "]" ) LIST1 one_term OPT ( "in" ident )
 | "match" ltac2_expr5 "with" OPT ltac2_branches "end"
+| "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5
 | qualid LIST1 tactic_arg
 ]