diff options
Diffstat (limited to 'plugins/decl_mode/g_decl_mode.ml4')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 03929b3b86..ef9d3159d2 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -19,6 +19,7 @@ open Tok (* necessary for camlp4 *) open Pcoq.Constr open Pcoq.Tactic +open Ppdecl_proof let pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in @@ -43,15 +44,6 @@ let pr_open_subgoals () = pr_subgoals close_cmd sigma goals *) -let pr_raw_proof_instr _ _ _ instr = - Errors.anomaly (Pp.str "Cannot print a proof_instr") - (* arnaud: Il nous faut quelque chose de type extr_genarg_printer si on veut aller - dans cette direction - Ppdecl_proof.pr_proof_instr (Global.env()) instr - *) -let pr_proof_instr _ _ _ instr = Empty.abort instr -let pr_glob_proof_instr _ _ _ instr = Empty.abort instr - let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= Decl_interp.interp_proof_instr (Decl_mode.get_info sigma gl) @@ -92,7 +84,7 @@ let vernac_proof_instr instr = (* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *) (* Only declared at raw level, because only used in vernac commands. *) -let wit_proof_instr : (raw_proof_instr, Empty.t, Empty.t) Genarg.genarg_type = +let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type = Genarg.make0 None "proof_instr" (* We create a new parser entry [proof_mode]. The Declarative proof mode |