diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 2 | ||||
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 2 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 |
3 files changed, 2 insertions, 4 deletions
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 88e62e46df..b5a2ac82eb 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -103,7 +103,7 @@ 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 "proof_instr" + Genarg.create_arg None "proof_instr" let _ = Tacinterp.add_interp_genarg "proof_instr" begin begin fun e x -> (* declares the globalisation function *) diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index f5b16e43fe..48bb87214a 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -134,8 +134,6 @@ TACTIC EXTEND firstorder | [ "firstorder" tactic_opt(t) firstorder_using(l) "with" ne_preident_list(l') ] -> [ gen_ground_tac true (Option.map eval_tactic t) l l' ] -| [ "firstorder" tactic_opt(t) ] -> - [ gen_ground_tac true (Option.map eval_tactic t) [] [] ] END TACTIC EXTEND gintuition diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index f330f9ff92..e8fec0dd84 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -154,7 +154,7 @@ type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Verna 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) = - Genarg.create_arg "function_rec_definition_loc" + Genarg.create_arg None "function_rec_definition_loc" VERNAC COMMAND EXTEND Function ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] -> [ |