diff options
| author | Pierre-Marie Pédrot | 2020-04-23 16:46:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-23 16:46:25 +0200 |
| commit | cddd0149b686b247116681a17b5c7bf42d513115 (patch) | |
| tree | f8696c9ad900efd1b54bd9ca84daddf12fdb580f /dev | |
| parent | 48f73e492465f3c46438583c069bc0ba745ef56f (diff) | |
| parent | 8de0fcaa08c82ece8874606e8fa1954d860bd88e (diff) | |
Merge PR #12130: [declare] [tactics] Move declare to `vernac`
Reviewed-by: ppedrot
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index 96a867475d..45e79147c1 100644 --- a/dev/base_include +++ b/dev/base_include @@ -129,7 +129,7 @@ open Elim open Equality open Hipattern open Inv -open Leminv +open Ltac_plugin.Leminv open Tacticals open Tactics open Eqschemes |