aboutsummaryrefslogtreecommitdiffstats
path: root/src/QInst.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/QInst.v')
-rw-r--r--src/QInst.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/QInst.v b/src/QInst.v
index 611973e..cb533ee 100644
--- a/src/QInst.v
+++ b/src/QInst.v
@@ -69,7 +69,7 @@ Ltac vauto :=
eapply impl_or_split_left; apply H
end;
apply H);
- auto.
+ auto with smtcoq_core.