diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/decl_expr.mli | 2 | ||||
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 1 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 1 | ||||
| -rw-r--r-- | plugins/quote/g_quote.ml4 | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.mli | 4 |
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 |