From 8a8fd265158fa3fe7eea65b50c3da722e81fa688 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Aug 2017 14:43:30 +0200
Subject: Binding more primitive tactics.

---
 tests/stuff/ltac2.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'tests')

diff --git a/tests/stuff/ltac2.v b/tests/stuff/ltac2.v
index ece6fca06a..6b30d42c09 100644
--- a/tests/stuff/ltac2.v
+++ b/tests/stuff/ltac2.v
@@ -143,3 +143,11 @@ Ltac2 rec do n tac := match Int.equal n 0 with
 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.on_hyps := None; Std.on_concl := Std.AllOccurrences }.
-- 
cgit v1.2.3