From 20831b39a73ebd38336f19ad4ddb4d6b1078d60d Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 31 Mar 2020 20:25:05 +0200 Subject: Compiles with Coq-8.10 --- src/QInst.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/QInst.v') 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. -- cgit