From 404baba955aa7bc4f5bc1cc357749d8e1cdc11c1 Mon Sep 17 00:00:00 2001 From: Patrick Nicodemus Date: Sun, 19 Jan 2025 12:36:15 -0500 Subject: [PATCH] tactics.v --- apps/eltac/theories/tactics.v | 1 + 1 file changed, 1 insertion(+) diff --git a/apps/eltac/theories/tactics.v b/apps/eltac/theories/tactics.v index dd8f1f3b1..874bbd1ba 100644 --- a/apps/eltac/theories/tactics.v +++ b/apps/eltac/theories/tactics.v @@ -1,4 +1,5 @@ From elpi.apps.eltac Require Export + apply intro constructor assumption