Integrate build and documentation of Ltac2

Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.

Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.

1 files changed, 143 insertions, 0 deletions

diff --git a/test-suite/ltac2/stuff/ltac2.v b/test-suite/ltac2/stuff/ltac2.v
new file mode 100644
index 0000000000..370bc70d15
--- /dev/null
+++ b/test-suite/ltac2/stuff/ltac2.v
@@ -0,0 +1,143 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 foo (_ : int) :=
+  let f (x : int) := x in
+  let _ := f 0 in
+  f 1.
+
+Print Ltac2 foo.
+
+Import Control.
+
+Ltac2 exact x := refine (fun () => x).
+
+Print Ltac2 refine.
+Print Ltac2 exact.
+
+Ltac2 foo' () := ident:(bla).
+
+Print Ltac2 foo'.
+
+Ltac2 bar x h := match x with
+| None => constr:(fun H => ltac2:(exact (hyp ident:(H))) -> nat)
+| Some x => x
+end.
+
+Print Ltac2 bar.
+
+Ltac2 qux := Some 0.
+
+Print Ltac2 qux.
+
+Ltac2 Type foo := [ Foo (int) ].
+
+Fail Ltac2 qux0 := Foo None.
+
+Ltac2 Type 'a ref := { mutable contents : 'a }.
+
+Fail Ltac2 qux0 := { contents := None }.
+Ltac2 foo0 () := { contents := None }.
+
+Print Ltac2 foo0.
+
+Ltac2 qux0 x := x.(contents).
+Ltac2 qux1 x := x.(contents) := x.(contents).
+
+Ltac2 qux2 := ([1;2], true).
+
+Print Ltac2 qux0.
+Print Ltac2 qux1.
+Print Ltac2 qux2.
+
+Import Control.
+
+Ltac2 qux3 x := constr:(nat -> ltac2:(refine (fun () => hyp x))).
+
+Print Ltac2 qux3.
+
+Ltac2 Type rec nat := [ O | S (nat) ].
+
+Ltac2 message_of_nat n :=
+let rec aux n :=
+match n with
+| O => Message.of_string "O"
+| S n => Message.concat (Message.of_string "S") (aux n)
+end in aux n.
+
+Print Ltac2 message_of_nat.
+
+Ltac2 numgoals () :=
+  let r := { contents := O } in
+  enter (fun () => r.(contents) := S (r.(contents)));
+  r.(contents).
+
+Print Ltac2 numgoals.
+
+Goal True /\ False.
+Proof.
+let n := numgoals () in Message.print (message_of_nat n).
+refine (fun () => open_constr:((fun x => conj _ _) 0)); ().
+let n := numgoals () in Message.print (message_of_nat n).
+
+Fail (hyp ident:(x)).
+Fail (enter (fun () => hyp ident:(There_is_no_spoon); ())).
+
+enter (fun () => Message.print (Message.of_string "foo")).
+
+enter (fun () => Message.print (Message.of_constr (goal ()))).
+Fail enter (fun () => Message.print (Message.of_constr (qux3 ident:(x)))).
+enter (fun () => plus (fun () => constr:(_); ()) (fun _ => ())).
+plus
+  (fun () => enter (fun () => let x := ident:(foo) in let _ := hyp x in ())) (fun _ => Message.print (Message.of_string "failed")).
+let x := { contents := 0 } in
+let x := x.(contents) := x.(contents) in x.
+Abort.
+
+Ltac2 Type exn ::= [ Foo ].
+
+Goal True.
+Proof.
+plus (fun () => zero Foo) (fun _ => ()).
+Abort.
+
+Ltac2 Type exn ::= [ Bar (string) ].
+
+Goal True.
+Proof.
+Fail zero (Bar "lol").
+Abort.
+
+Ltac2 Notation "refine!" c(thunk(constr)) := refine c.
+
+Goal True.
+Proof.
+refine! I.
+Abort.
+
+Goal True.
+Proof.
+let x () := plus (fun () => 0) (fun _ => 1) in
+match case x with
+| Val x =>
+  match x with
+  | (x, k) => Message.print (Message.of_int (k Not_found))
+  end
+| Err x => Message.print (Message.of_string "Err")
+end.
+Abort.
+
+Goal (forall n : nat, n = 0 -> False) -> True.
+Proof.
+refine (fun () => '(fun H => _)).
+Std.case true (hyp @H, Std.ExplicitBindings [Std.NamedHyp @n, '0]).
+refine (fun () => 'eq_refl).
+Qed.
+
+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 := true; Std.rConst := [];
+} { Std.on_hyps := None; Std.on_concl := Std.AllOccurrences }.
+Abort.