From 39cc672b0fdf31cfef816fd14b76e43bff7e6da2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 24 Sep 2015 08:52:37 +0200
Subject: Fix compilation on 8.5

---
 mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
index 1b4afb2..e6636cb 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
@@ -6075,7 +6075,7 @@ GEXTEND Gram
           let s = coerce_reference_to_id qid in
 	  Vernacexpr.VernacDefinition
 	    ((Some Decl_kinds.Global,Decl_kinds.CanonicalStructure),
-             (dummy_loc,s),(d  ))
+             ((dummy_loc,s),None),(d  ))
   ]];
 END
 
-- 
cgit v1.2.3