diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-06-07 13:19:30 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-06-07 13:19:30 +0200 |
commit | 4d521764d1062a10f108086cc1bde4ba62e16b08 (patch) | |
tree | ced8a902851c50b28bf7b4432bd09860ef643fc9 /src/QInst.v | |
parent | 75f83354b9c9f0f8fd25d4faba6a6825625d5924 (diff) | |
download | smtcoq-4d521764d1062a10f108086cc1bde4ba62e16b08.tar.gz smtcoq-4d521764d1062a10f108086cc1bde4ba62e16b08.zip |
Port the Coq part
Diffstat (limited to 'src/QInst.v')
-rw-r--r-- | src/QInst.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/QInst.v b/src/QInst.v index b2dd836..e78a2fe 100644 --- a/src/QInst.v +++ b/src/QInst.v @@ -27,7 +27,7 @@ Proof. installed when we compile SMTCoq. *) Qed. -Hint Resolve impl_split : smtcoq_core. +#[export] Hint Resolve impl_split : smtcoq_core. (** verit silently transforms an <implb (a || b) c> into a <or (not a) c> or into a <or (not b) c> when instantiating such a quantified theorem *) |