Change the toplevel representation of Ltac values to an untyped one.

This brings the evaluation model of Ltac closer to those of usual languages, and
further allows the integration of static typing in the long run. More precisely,
toplevel constructed values such as lists and the like do not carry anymore the
type of the underlying data they contain.

This is mostly an API change, as it did not break any contrib outside of mathcomp.

5 files changed, 6 insertions, 4 deletions

diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 9d78a51ef..29ecb94ca 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/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 587d10d1c..b04c4a50c 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
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index e93c395e3..0ba18f568 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
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index a15b0eb05..e4c8da93b 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 07a1ae833..ca6aba9a0 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