More examples

2 files changed, 48 insertions, 12 deletions

diff --git a/tests/stuff/ltac2.v b/tests/stuff/ltac2.v
index 6b30d42c09..95bff7e569 100644
--- a/tests/stuff/ltac2.v
+++ b/tests/stuff/ltac2.v
@@ -55,10 +55,6 @@ Ltac2 qux3 x := constr:(nat -> ltac2:(refine (fun () => hyp x))).
 
 Print Ltac2 qux3.
 
-Ltac2 qux4 f x := x, (f x, x).
-
-Print Ltac2 qux4.
-
 Ltac2 Type rec nat := [ O | S (nat) ].
 
 Ltac2 message_of_nat n :=
@@ -137,17 +133,10 @@ Std.ecase (hyp @H, Std.ExplicitBindings [Std.NamedHyp @n, '0]).
 refine (fun () => 'eq_refl).
 Qed.
 
-Ltac2 rec do n tac := match Int.equal n 0 with
-| true => ()
-| false => tac (); do (Int.sub n 1) tac
-end.
-
-Print Ltac2 do.
-
 Goal forall x, 1 + x = x + 1.
 Proof.
 refine (fun () => '(fun x => _)).
 Std.cbv {
   Std.rBeta := true; Std.rMatch := true; Std.rFix := true; Std.rCofix := true;
-  Std.rZeta := true; Std.rDelta := false; rConst := [];
+  Std.rZeta := true; Std.rDelta := false; Std.rConst := [];
 } { Std.on_hyps := None; Std.on_concl := Std.AllOccurrences }.
diff --git a/tests/typing.v b/tests/typing.v
index 8460ab42b7..9f18292716 100644
--- a/tests/typing.v
+++ b/tests/typing.v
@@ -14,6 +14,10 @@ Fail Ltac2 test2 () := test0 true.
 
 Fail Ltac2 test2 () := test0 0 0.
 
+Ltac2 test3 f x := x, (f x, x).
+
+Print Ltac2 test3.
+
 (** Polymorphism *)
 
 Ltac2 rec list_length l :=
@@ -23,3 +27,46 @@ match l with
 end.
 
 Print Ltac2 list_length.
+
+(** Pattern-matching *)
+
+Ltac2 ifb b f g := match b with
+| true => f ()
+| false => g ()
+end.
+
+Print Ltac2 ifb.
+
+Ltac2 if_not_found e f g := match e with
+| Not_found => f ()
+| _ => g ()
+end.
+
+Fail Ltac2 ifb' b f g := match b with
+| true => f ()
+end.
+
+Fail Ltac2 if_not_found' e f g := match e with
+| Not_found => f ()
+end.
+
+(** Reimplementing 'do'. Return value of the function useless. *)
+
+Ltac2 rec do n tac := match Int.equal n 0 with
+| true => ()
+| false => tac (); do (Int.sub n 1) tac
+end.
+
+Print Ltac2 do.
+
+(** Non-function pure values are OK. *)
+
+Ltac2 tuple0 := ([1; 2], true, (fun () => "yay")).
+
+Print Ltac2 tuple0.
+
+(** Impure values are not. *)
+
+Fail Ltac2 not_a_value := { contents := 0 }.
+Fail Ltac2 not_a_value := "nope".
+Fail Ltac2 not_a_value := list_length [].