Prepare merge into Coq

11 files changed, 0 insertions, 774 deletions

diff --git a/tests/Makefile b/tests/Makefile
deleted file mode 100644
index d85ae90dd6..0000000000
--- a/tests/Makefile
+++ /dev/null
@@ -1,16 +0,0 @@
-ifeq "$(COQBIN)" ""
-  COQBIN=$(dir $(shell which coqc))/
-endif
-
-all: $(patsubst %.v,%.v.log,$(wildcard *.v))
-
-%.v.log: %.v
-	$(COQBIN)/coqc -I ../src -Q ../theories Ltac2 $< > $@
-	if [ $$? = 0 ]; then \
-		echo "    $<... OK"; \
-	else \
-		echo "    $<... FAIL!"; \
-	fi; \
-
-clean:
-	rm -f *.log
diff --git a/tests/compat.v b/tests/compat.v
deleted file mode 100644
index 489fa638e4..0000000000
--- a/tests/compat.v
+++ /dev/null
@@ -1,58 +0,0 @@
-Require Import Ltac2.Ltac2.
-
-Import Ltac2.Notations.
-
-(** Test calls to Ltac1 from Ltac2 *)
-
-Ltac2 foo () := ltac1:(discriminate).
-
-Goal true = false -> False.
-Proof.
-foo ().
-Qed.
-
-Goal true = false -> false = true.
-Proof.
-intros H; ltac1:(match goal with [ H : ?P |- _ ] => rewrite H end); reflexivity.
-Qed.
-
-Goal true = false -> false = true.
-Proof.
-intros H; ltac1:(rewrite H); reflexivity.
-Abort.
-
-(** Variables do not cross the compatibility layer boundary. *)
-Fail Ltac2 bar nay := ltac1:(discriminate nay).
-
-Fail Ltac2 pose1 (v : constr) :=
-  ltac1:(pose $v).
-
-(** Test calls to Ltac2 from Ltac1 *)
-
-Set Default Proof Mode "Classic".
-
-Ltac foo := ltac2:(foo ()).
-
-Goal true = false -> False.
-Proof.
-ltac2:(foo ()).
-Qed.
-
-Goal true = false -> False.
-Proof.
-foo.
-Qed.
-
-(** Variables do not cross the compatibility layer boundary. *)
-Fail Ltac bar x := ltac2:(foo x).
-
-Ltac mytac tac := idtac "wow".
-
-Goal True.
-Proof.
-(** Fails because quotation is evaluated eagerly *)
-Fail mytac ltac2:(fail).
-(** One has to thunk thanks to the idtac trick *)
-let t := idtac; ltac2:(fail) in mytac t.
-constructor.
-Qed.
diff --git a/tests/errors.v b/tests/errors.v
deleted file mode 100644
index c677f6af5d..0000000000
--- a/tests/errors.v
+++ /dev/null
@@ -1,12 +0,0 @@
-Require Import Ltac2.Ltac2.
-
-Goal True.
-Proof.
-let x := Control.plus
-  (fun () => let _ := constr:(nat -> 0) in 0)
-  (fun e => match e with Not_found => 1 | _ => 2 end) in
-match Int.equal x 2 with
-| true => ()
-| false => Control.throw (Tactic_failure None)
-end.
-Abort.
diff --git a/tests/example1.v b/tests/example1.v
deleted file mode 100644
index 023791050f..0000000000
--- a/tests/example1.v
+++ /dev/null
@@ -1,27 +0,0 @@
-Require Import Ltac2.Ltac2.
-
-Import Ltac2.Control.
-
-(** Alternative implementation of the hyp primitive *)
-Ltac2 get_hyp_by_name x :=
-  let h := hyps () in
-  let rec find x l := match l with
-  | [] => zero Not_found
-  | p :: l =>
-    match p with
-    | (id, _, t) =>
-      match Ident.equal x id with
-      | true => t
-      | false => find x l
-      end
-    end
-  end in
-  find x h.
-
-Print Ltac2 get_hyp_by_name.
-
-Goal forall n m, n + m = 0 -> n = 0.
-Proof.
-refine (fun () => '(fun n m H => _)).
-let t := get_hyp_by_name @H in Message.print (Message.of_constr t).
-Abort.
diff --git a/tests/example2.v b/tests/example2.v
deleted file mode 100644
index c953d25061..0000000000
--- a/tests/example2.v
+++ /dev/null
@@ -1,281 +0,0 @@
-Require Import Ltac2.Ltac2.
-
-Import Ltac2.Notations.
-
-Set Default Goal Selector "all".
-
-Goal exists n, n = 0.
-Proof.
-split with (x := 0).
-reflexivity.
-Qed.
-
-Goal exists n, n = 0.
-Proof.
-split with 0.
-split.
-Qed.
-
-Goal exists n, n = 0.
-Proof.
-let myvar := Std.NamedHyp @x in split with ($myvar := 0).
-split.
-Qed.
-
-Goal (forall n : nat, n = 0 -> False) -> True.
-Proof.
-intros H.
-eelim &H.
-split.
-Qed.
-
-Goal (forall n : nat, n = 0 -> False) -> True.
-Proof.
-intros H.
-elim &H with 0.
-split.
-Qed.
-
-Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> P 0.
-Proof.
-intros P H.
-Fail apply &H.
-apply &H with (m := 0).
-split.
-Qed.
-
-Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> (0 = 1) -> P 0.
-Proof.
-intros P H e.
-apply &H with (m := 1) in e.
-exact e.
-Qed.
-
-Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> P 0.
-Proof.
-intros P H.
-eapply &H.
-split.
-Qed.
-
-Goal exists n, n = 0.
-Proof.
-Fail constructor 1.
-constructor 1 with (x := 0).
-split.
-Qed.
-
-Goal exists n, n = 0.
-Proof.
-econstructor 1.
-split.
-Qed.
-
-Goal forall n, 0 + n = n.
-Proof.
-intros n.
-induction &n as [|n] using nat_rect; split.
-Qed.
-
-Goal forall n, 0 + n = n.
-Proof.
-intros n.
-let n := @X in
-let q := Std.NamedHyp @P in
-induction &n as [|$n] using nat_rect with ($q := fun m => 0 + m = m); split.
-Qed.
-
-Goal forall n, 0 + n = n.
-Proof.
-intros n.
-destruct &n as [|n] using nat_rect; split.
-Qed.
-
-Goal forall n, 0 + n = n.
-Proof.
-intros n.
-let n := @X in
-let q := Std.NamedHyp @P in
-destruct &n as [|$n] using nat_rect with ($q := fun m => 0 + m = m); split.
-Qed.
-
-Goal forall b1 b2, andb b1 b2 = andb b2 b1.
-Proof.
-intros b1 b2.
-destruct &b1 as [|], &b2 as [|]; split.
-Qed.
-
-Goal forall n m, n = 0 -> n + m = m.
-Proof.
-intros n m Hn.
-rewrite &Hn; split.
-Qed.
-
-Goal forall n m p, n = m -> p = m -> 0 = n -> p = 0.
-Proof.
-intros n m p He He' Hn.
-rewrite &He, <- &He' in Hn.
-rewrite &Hn.
-split.
-Qed.
-
-Goal forall n m, (m = n -> n = m) -> m = n -> n = 0 -> m = 0.
-Proof.
-intros n m He He' He''.
-rewrite <- &He by assumption.
-Control.refine (fun () => &He'').
-Qed.
-
-Goal forall n (r := if true then n else 0), r = n.
-Proof.
-intros n r.
-hnf in r.
-split.
-Qed.
-
-Goal 1 = 0 -> 0 = 0.
-Proof.
-intros H.
-pattern 0 at 1.
-let occ := 2 in pattern 1 at 1, 0 at $occ in H.
-reflexivity.
-Qed.
-
-Goal 1 + 1 = 2.
-Proof.
-vm_compute.
-reflexivity.
-Qed.
-
-Goal 1 + 1 = 2.
-Proof.
-native_compute.
-reflexivity.
-Qed.
-
-Goal 1 + 1 = 2 - 0 -> True.
-Proof.
-intros H.
-vm_compute plus in H.
-reflexivity.
-Qed.
-
-Goal 1 = 0 -> True /\ True.
-Proof.
-intros H.
-split; fold (1 + 0) (1 + 0) in H.
-reflexivity.
-Qed.
-
-Goal 1 + 1 = 2.
-Proof.
-cbv [ Nat.add ].
-reflexivity.
-Qed.
-
-Goal 1 + 1 = 2.
-Proof.
-let x := reference:(Nat.add) in
-cbn beta iota delta [ $x ].
-reflexivity.
-Qed.
-
-Goal 1 + 1 = 2.
-Proof.
-simpl beta.
-reflexivity.
-Qed.
-
-Goal 1 + 1 = 2.
-Proof.
-lazy.
-reflexivity.
-Qed.
-
-Goal let x := 1 + 1 - 1 in x = x.
-Proof.
-intros x.
-unfold &x at 1.
-let x := reference:(Nat.sub) in unfold Nat.add, $x in x.
-reflexivity.
-Qed.
-
-Goal exists x y : nat, x = y.
-Proof.
-exists 0, 0; reflexivity.
-Qed.
-
-Goal exists x y : nat, x = y.
-Proof.
-eexists _, 0; reflexivity.
-Qed.
-
-Goal exists x y : nat, x = y.
-Proof.
-refine '(let x := 0 in _).
-eexists; exists &x; reflexivity.
-Qed.
-
-Goal True.
-Proof.
-pose (X := True).
-constructor.
-Qed.
-
-Goal True.
-Proof.
-pose True as X.
-constructor.
-Qed.
-
-Goal True.
-Proof.
-let x := @foo in
-set ($x := True) in * |-.
-constructor.
-Qed.
-
-Goal 0 = 0.
-Proof.
-remember 0 as n eqn: foo at 1.
-rewrite foo.
-reflexivity.
-Qed.
-
-Goal True.
-Proof.
-assert (H := 0 + 0).
-constructor.
-Qed.
-
-Goal True.
-Proof.
-assert (exists n, n = 0) as [n Hn].
-+ exists 0; reflexivity.
-+ exact I.
-Qed.
-
-Goal True -> True.
-Proof.
-assert (H : 0 + 0 = 0) by reflexivity.
-intros x; exact x.
-Qed.
-
-Goal 1 + 1 = 2.
-Proof.
-change (?a + 1 = 2) with (2 = $a + 1).
-reflexivity.
-Qed.
-
-Goal (forall n, n = 0 -> False) -> False.
-Proof.
-intros H.
-specialize (H 0 eq_refl).
-destruct H.
-Qed.
-
-Goal (forall n, n = 0 -> False) -> False.
-Proof.
-intros H.
-specialize (H 0 eq_refl) as [].
-Qed.
diff --git a/tests/matching.v b/tests/matching.v
deleted file mode 100644
index 4338cbd32f..0000000000
--- a/tests/matching.v
+++ /dev/null
@@ -1,71 +0,0 @@
-Require Import Ltac2.Ltac2 Ltac2.Notations.
-
-Ltac2 Type exn ::= [ Nope ].
-
-Ltac2 check_id id id' := match Ident.equal id id' with
-| true => ()
-| false => Control.throw Nope
-end.
-
-Goal True -> False.
-Proof.
-Fail
-let b := { contents := true } in
-let f c :=
-  match b.(contents) with
-  | true => Message.print (Message.of_constr c); b.(contents) := false; fail
-  | false => ()
-  end
-in
-(** This fails because the matching is not allowed to backtrack once
-    it commits to a branch*)
-lazy_match! '(nat -> bool) with context [?a] => f a end.
-lazy_match! Control.goal () with ?a -> ?b => Message.print (Message.of_constr b) end.
-
-(** This one works by taking the second match context, i.e. ?a := nat *)
-let b := { contents := true } in
-let f c :=
-  match b.(contents) with
-  | true => b.(contents) := false; fail
-  | false => Message.print (Message.of_constr c)
-  end
-in
-match! '(nat -> bool) with context [?a] => f a end.
-Abort.
-
-Goal forall (i j : unit) (x y : nat) (b : bool), True.
-Proof.
-Fail match! goal with
-| [ h : ?t, h' : ?t |- _ ] => ()
-end.
-intros i j x y b.
-match! goal with
-| [ h : ?t, h' : ?t |- _ ] =>
-  check_id h @x;
-  check_id h' @y
-end.
-match! reverse goal with
-| [ h : ?t, h' : ?t |- _ ] =>
-  check_id h @j;
-  check_id h' @i
-end.
-Abort.
-
-(* Check #79 *)
-Goal 2 = 3.
-  Control.plus
-    (fun ()
-     => lazy_match! goal with
-    | [ |- 2 = 3 ] => Control.zero (Tactic_failure None)
-    | [ |- 2 = _ ] => Control.zero (Tactic_failure (Some (Message.of_string "should not be printed")))
-     end)
-    (fun e
-     => match e with
-        | Tactic_failure c
-          => match c with
-             | None => ()
-             | _ => Control.zero e
-             end
-        | e => Control.zero e
-        end).
-Abort.
diff --git a/tests/quot.v b/tests/quot.v
deleted file mode 100644
index 624c4ad0c1..0000000000
--- a/tests/quot.v
+++ /dev/null
@@ -1,26 +0,0 @@
-Require Import Ltac2.Ltac2.
-
-(** Test for quotations *)
-
-Ltac2 ref0 () := reference:(&x).
-Ltac2 ref1 () := reference:(nat).
-Ltac2 ref2 () := reference:(Datatypes.nat).
-Fail Ltac2 ref () := reference:(i_certainly_dont_exist).
-Fail Ltac2 ref () := reference:(And.Me.neither).
-
-Goal True.
-Proof.
-let x := constr:(I) in
-let y := constr:((fun z => z) $x) in
-Control.refine (fun _ => y).
-Qed.
-
-Goal True.
-Proof.
-(** Here, Ltac2 should not put its variables in the same environment as
-    Ltac1 otherwise the second binding fails as x is bound but not an
-    ident. *)
-let x := constr:(I) in
-let y := constr:((fun x => x) $x) in
-Control.refine (fun _ => y).
-Qed.
diff --git a/tests/rebind.v b/tests/rebind.v
deleted file mode 100644
index e1c20a2059..0000000000
--- a/tests/rebind.v
+++ /dev/null
@@ -1,34 +0,0 @@
-Require Import Ltac2.Ltac2 Ltac2.Notations.
-
-Ltac2 mutable foo () := constructor.
-
-Goal True.
-Proof.
-foo ().
-Qed.
-
-Ltac2 Set foo := fun _ => fail.
-
-Goal True.
-Proof.
-Fail foo ().
-constructor.
-Qed.
-
-(** Not the right type *)
-Fail Ltac2 Set foo := 0.
-
-Ltac2 bar () := ().
-
-(** Cannot redefine non-mutable tactics *)
-Fail Ltac2 Set bar := fun _ => ().
-
-(** Subtype check *)
-
-Ltac2 mutable rec f x := f x.
-
-Fail Ltac2 Set f := fun x => x.
-
-Ltac2 mutable g x := x.
-
-Ltac2 Set g := f.
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.
diff --git a/tests/tacticals.v b/tests/tacticals.v
deleted file mode 100644
index 1a2fbcbb37..0000000000
--- a/tests/tacticals.v
+++ /dev/null
@@ -1,34 +0,0 @@
-Require Import Ltac2.Ltac2.
-
-Import Ltac2.Notations.
-
-Goal True.
-Proof.
-Fail fail.
-Fail solve [ () ].
-try fail.
-repeat fail.
-repeat ().
-solve [ constructor ].
-Qed.
-
-Goal True.
-Proof.
-first [
-  Message.print (Message.of_string "Yay"); fail
-| constructor
-| Message.print (Message.of_string "I won't be printed")
-].
-Qed.
-
-Goal True /\ True.
-Proof.
-Fail split > [ split | |].
-split > [split | split].
-Qed.
-
-Goal True /\ (True -> True) /\ True.
-Proof.
-split > [ | split] > [split | .. | split].
-intros H; refine &H.
-Qed.
diff --git a/tests/typing.v b/tests/typing.v
deleted file mode 100644
index 9f18292716..0000000000
--- a/tests/typing.v
+++ /dev/null
@@ -1,72 +0,0 @@
-Require Import Ltac2.Ltac2.
-
-(** Ltac2 is typed à la ML. *)
-
-Ltac2 test0 n := Int.add n 1.
-
-Print Ltac2 test0.
-
-Ltac2 test1 () := test0 0.
-
-Print Ltac2 test1.
-
-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 :=
-match l with
-| [] => 0
-| x :: l => Int.add 1 (list_length l)
-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 [].