Fix compilation on 8.5

math-comp · Sep 24, 2015 · 39cc672 · 39cc672
1 parent ade7c12
commit 39cc672
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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