diff options
Diffstat (limited to 'cparser')
| -rw-r--r-- | cparser/validator/Interpreter_complete.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/cparser/validator/Interpreter_complete.v b/cparser/validator/Interpreter_complete.v index eb407061..ff88571b 100644 --- a/cparser/validator/Interpreter_complete.v +++ b/cparser/validator/Interpreter_complete.v @@ -14,6 +14,7 @@ (* *********************************************************************) Require Import Streams. +Require Import ProofIrrelevance. Require Import Equality. Require Import List. Require Import Syntax. |