From e73d5db97cdb22cce2ee479469f62af3c4b6264a Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 8 Jul 2016 14:43:57 +0200
Subject: Port to Coq 8.5pl2

Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
---
 cfrontend/SimplLocalsproof.v | 1 -
 1 file changed, 1 deletion(-)

(limited to 'cfrontend/SimplLocalsproof.v')

diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 2cd82d8f..48a7a773 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -2291,4 +2291,3 @@ Local Transparent Linker_fundef.
             type_eq t0 t2 && calling_convention_eq c c0); inv H2.
   econstructor; split; eauto. 
 Qed.
-
-- 
cgit