From 2537e84ba9fa92db6cfd3d7f5e400b1716c31246 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 17 Mar 2016 14:42:51 +0100
Subject: Removing the registering of default values for generic arguments.

---
 plugins/decl_mode/g_decl_mode.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index b62cfd6add..2d096a1081 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -87,7 +87,7 @@ let vernac_proof_instr instr =
 
 (* Only declared at raw level, because only used in vernac commands. *)
 let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type =
-  Genarg.make0 None "proof_instr"
+  Genarg.make0 "proof_instr"
 
 (* We create a new parser entry [proof_mode]. The Declarative proof mode
     will replace the normal parser entry for tactics with this one. *)
-- 
cgit v1.2.3