From a2a8840a4fe1b3d6c6dbc27b5521b28bd319ff42 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 14 Apr 2016 20:43:57 +0200
Subject: More toplevel value representation sharing.

---
 interp/stdarg.ml            | 2 +-
 ltac/extratactics.ml4       | 8 +-------
 plugins/funind/g_indfun.ml4 | 1 +
 3 files changed, 3 insertions(+), 8 deletions(-)

diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 9e85dbaf38..2a7d52e3af 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -27,7 +27,7 @@ let wit_string : string uniform_genarg_type =
   make0 "string"
 
 let wit_pre_ident : string uniform_genarg_type =
-  make0 "preident"
+  make0 ~dyn:(val_tag (topwit wit_string)) "preident"
 
 (** Aliases for compatibility *)
 
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index eda530c265..925c1679f2 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -938,12 +938,6 @@ type cmp =
 type 'i test =
   | Test of cmp * 'i * 'i
 
-let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 "cmp"
-let _ = Geninterp.register_val0 wit_cmp None
-let wit_test : (int or_var test,int or_var test,int test) Genarg.genarg_type =
-  Genarg.make0 "tactest"
-let _ = Geninterp.register_val0 wit_test None
-
 let pr_cmp = function
   | Eq -> Pp.str"="
   | Lt -> Pp.str"<"
@@ -966,7 +960,7 @@ let pr_itest' _prc _prlc _prt = pr_itest
 
 
 
-ARGUMENT EXTEND comparison TYPED AS cmp PRINTED BY pr_cmp'
+ARGUMENT EXTEND comparison PRINTED BY pr_cmp'
 | [ "="  ] -> [ Eq ]
 | [ "<"  ] -> [ Lt ]
 | [ "<=" ] -> [ Le ]
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index e93c395e3d..0ba18f568a 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -65,6 +65,7 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
 
 
 ARGUMENT EXTEND fun_ind_using
+  TYPED AS constr_with_bindings option
   PRINTED BY pr_fun_ind_using_typed
   RAW_TYPED AS constr_with_bindings_opt
   RAW_PRINTED BY pr_fun_ind_using
-- 
cgit v1.2.3