diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 16 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 6 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 4 |
3 files changed, 11 insertions, 15 deletions
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 70338c52b5..291fabdb6e 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -100,27 +100,25 @@ let proof_instr = Gram.entry_create "proofmode:instr" (* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *) (* [Genarg.create_arg] creates a new embedding into Genarg. *) -let (wit_proof_instr,globwit_proof_instr,rawwit_proof_instr) = +let wit_proof_instr = Genarg.create_arg None "proof_instr" let _ = Tacintern.add_intern_genarg "proof_instr" begin fun e x -> (* declares the globalisation function *) - Genarg.in_gen globwit_proof_instr - (Decl_interp.intern_proof_instr e (Genarg.out_gen rawwit_proof_instr x)) + Genarg.in_gen (Genarg.glbwit wit_proof_instr) + (Decl_interp.intern_proof_instr e (Genarg.out_gen (Genarg.rawwit wit_proof_instr) x)) end let _ = Tacinterp.add_interp_genarg "proof_instr" begin fun ist gl x -> (* declares the interpretation function *) Tacmach.project gl , - Genarg.in_gen wit_proof_instr - (interp_proof_instr ist gl (Genarg.out_gen globwit_proof_instr x)) + Genarg.in_gen (Genarg.topwit wit_proof_instr) + (interp_proof_instr ist gl (Genarg.out_gen (Genarg.glbwit wit_proof_instr) x)) end (* declares the substitution function, irrelevant in our case : *) let _ = Tacsubst.add_genarg_subst "proof_instr" (fun _ x -> x) -let _ = Pptactic.declare_extra_genarg_pprule - (rawwit_proof_instr, pr_raw_proof_instr) - (globwit_proof_instr, pr_glob_proof_instr) - (wit_proof_instr, pr_proof_instr) +let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr + pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr (* We use the VERNAC EXTEND facility with a custom non-terminal to populate [proof_mode] with a new toplevel interpreter. diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 088b4a0cde..8b90824fd2 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -151,11 +151,9 @@ GEXTEND Gram ; END -type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located, 'a) Genarg.abstract_argument_type +type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located -let (wit_function_rec_definition_loc : Genarg.tlevel function_rec_definition_loc_argtype), - (globwit_function_rec_definition_loc : Genarg.glevel function_rec_definition_loc_argtype), - (rawwit_function_rec_definition_loc : Genarg.rlevel function_rec_definition_loc_argtype) = +let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) = Genarg.create_arg None "function_rec_definition_loc" VERNAC COMMAND EXTEND Function ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] -> diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index b6b69ec2d0..5556912ebb 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -129,8 +129,8 @@ let closed_term_ast l = let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in TacFun([Some(Id.of_string"t")], TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term", - [Genarg.in_gen Genarg.globwit_constr (GVar(Loc.ghost,Id.of_string"t"),None); - Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l]))) + [Genarg.in_gen (Genarg.glbwit Genarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None); + Genarg.in_gen (Genarg.glbwit (Genarg.wit_list1 Genarg.wit_ref)) l]))) (* let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" *) |