Prepare merge into Coq

1 files changed, 0 insertions, 143 deletions

diff --git a/tests/stuff/ltac2.v b/tests/stuff/ltac2.v
deleted file mode 100644
index 370bc70d15..0000000000
--- a/tests/stuff/ltac2.v
+++ /dev/null
@@ -1,143 +0,0 @@
-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.