diff options
Diffstat (limited to 'plugins/decl_mode/g_decl_mode.ml4')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index fd98d5457..045678f0c 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -111,6 +111,7 @@ let _ = Tacinterp.add_interp_genarg "proof_instr" (Decl_interp.intern_proof_instr e (Genarg.out_gen rawwit_proof_instr x)) end, 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, |