From 320f39edca5061b84a8a45b5c33e516049c7f7fe Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 21 Sep 2016 13:27:28 +0200 Subject: Fix minor issues in some proofs and tactics. These minor problems were revealed by porting CompCert to Coq 8.6, where they trigger errors. --- cparser/validator/Interpreter_complete.v | 1 + 1 file changed, 1 insertion(+) (limited to 'cparser/validator') 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. -- cgit