diff options
| author | letouzey | 2012-10-16 16:24:23 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-16 16:24:23 +0000 |
| commit | 15daaa856a6dd1f97845c4f24fe27eaf4cdbdda0 (patch) | |
| tree | 0b5a33550e30f286ef65e7c12ea452c2b86da409 /plugins/decl_mode/g_decl_mode.ml4 | |
| parent | 3b5927180128a4e8f10f7437641ff3af220194b3 (diff) | |
Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15896 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/decl_mode/g_decl_mode.ml4')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index a3052320cf..c2b286f1b3 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -102,19 +102,20 @@ let proof_instr = Gram.entry_create "proofmode:instr" (* [Genarg.create_arg] creates a new embedding into Genarg. *) let (wit_proof_instr,globwit_proof_instr,rawwit_proof_instr) = Genarg.create_arg None "proof_instr" -let _ = Tacinterp.add_interp_genarg "proof_instr" - begin +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)) - end, + 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)) - end, - begin fun _ x -> x end (* declares the substitution function, irrelevant in our case *) - end + 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) |