diff options
Diffstat (limited to 'src/common/Maps.v')
| -rw-r--r-- | src/common/Maps.v | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/src/common/Maps.v b/src/common/Maps.v index 696c9b8..f0f264d 100644 --- a/src/common/Maps.v +++ b/src/common/Maps.v @@ -17,13 +17,15 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From vericert Require Import Vericertlib. +Set Implicit Arguments. -From compcert Require Export Maps. -From compcert Require Import Errors. -Import PTree. +Require Export compcert.lib.Maps. -Set Implicit Arguments. +Require Import compcert.common.Errors. + +Require Import vericert.common.Vericertlib. + +Import PTree. Local Open Scope error_monad_scope. |