From de4b9b68445d9f3e48da789404cbdfcd89214585 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 18 Apr 2016 14:39:34 +0200
Subject: Moving the Val module to Geninterp.

---
 plugins/decl_mode/decl_expr.mli | 2 +-
 plugins/quote/g_quote.ml4       | 2 +-
 plugins/setoid_ring/newring.mli | 4 ++--
 3 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 9d78a51ef6..29ecb94ca8 100644
--- a/plugins/decl_mode/decl_expr.mli
+++ b/plugins/decl_mode/decl_expr.mli
@@ -99,4 +99,4 @@ type proof_instr =
     (Term.constr statement,
      Term.constr,
      proof_pattern,
-     Genarg.Val.t) gen_proof_instr
+     Geninterp.Val.t) gen_proof_instr
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index a15b0eb05a..e4c8da93b1 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -24,7 +24,7 @@ let loc = Loc.ghost
 let cont = Id.of_string "cont"
 let x = Id.of_string "x"
 
-let make_cont (k : Genarg.Val.t) (c : Constr.t) =
+let make_cont (k : Val.t) (c : Constr.t) =
   let c = Tacinterp.Value.of_constr c in
   let tac = TacCall (loc, ArgVar (loc, cont), [Reference (ArgVar (loc, x))]) in
   let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index 07a1ae833b..ca6aba9a0f 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -45,7 +45,7 @@ val ic : constr_expr -> Evd.evar_map * constr
 val from_name : ring_info Spmap.t ref
 
 val ring_lookup :
-  Genarg.Val.t ->
+  Geninterp.Val.t ->
   constr list ->
   constr list -> constr -> unit Proofview.tactic
 
@@ -73,6 +73,6 @@ val add_field_theory :
 val field_from_name : field_info Spmap.t ref
 
 val field_lookup :
-  Genarg.Val.t ->
+  Geninterp.Val.t ->
   constr list ->
   constr list -> constr -> unit Proofview.tactic
-- 
cgit v1.2.3


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.

---
 plugins/funind/g_indfun.ml4 | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins')

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


From 729d838838d8df06395726477817620e2ae998bc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 20 Apr 2016 17:24:58 +0200
Subject: Interpretation function can return any untyped value.

---
 plugins/firstorder/g_ground.ml4 | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins')

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 587d10d1cc..b04c4a50c9 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -122,6 +122,7 @@ let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma
 let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
 
 ARGUMENT EXTEND firstorder_using
+  TYPED AS reference_list
   PRINTED BY pr_firstorder_using_typed
   RAW_TYPED AS reference_list
   RAW_PRINTED BY pr_firstorder_using_raw
-- 
cgit v1.2.3