try out a new Coq 8.5 syntax to shorten long Import lines

15be7b25 · Ralf Jung · c78daf89 · 15be7b25
Commit 15be7b25 authored Feb 13, 2016 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

heap_lang/tests.v heap_lang/tests.v +1 -1

No files found.
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
 (** This file is essentially a bunch of testcases. *)
 Require Import program_logic.ownership.
-Require Import heap_lang.substitution heap_lang.tactics heap_lang.notation.
+From heap_lang Require Import substitution tactics notation.
 Import uPred.

 Module LangTests.