diff options
Diffstat (limited to 'plugins/funind/g_indfun.ml4')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 57 |
1 files changed, 32 insertions, 25 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index a15e46bf..42e49031 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -9,15 +9,16 @@ open Compat open Util open Term -open Vars -open Names open Pp open Constrexpr open Indfun_common open Indfun open Genarg -open Tacticals +open Constrarg open Misctypes +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic DECLARE PLUGIN "recdef_plugin" @@ -55,10 +56,13 @@ let pr_with_bindings_typed prc prlc (c,bl) = let pr_fun_ind_using_typed prc prlc _ opt_c = match opt_c with | None -> mt () - | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b.Evd.it) + | Some b -> + let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in + spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b) ARGUMENT EXTEND fun_ind_using + TYPED AS constr_with_bindings option PRINTED BY pr_fun_ind_using_typed RAW_TYPED AS constr_with_bindings_opt RAW_PRINTED BY pr_fun_ind_using @@ -86,9 +90,9 @@ let pr_intro_as_pat _prc _ _ pat = let out_disjunctive = function | loc, IntroAction (IntroOrAndPattern l) -> (loc,l) - | _ -> Errors.error "Disjunctive or conjunctive intro pattern expected." + | _ -> CErrors.error "Disjunctive or conjunctive intro pattern expected." -ARGUMENT EXTEND with_names TYPED AS simple_intropattern_opt PRINTED BY pr_intro_as_pat +ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat | [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] | [] ->[ None ] END @@ -119,12 +123,12 @@ TACTIC EXTEND snewfunind END -let pr_constr_coma_sequence prc _ _ = prlist_with_sep pr_comma prc +let pr_constr_comma_sequence prc _ _ = prlist_with_sep pr_comma prc -ARGUMENT EXTEND constr_coma_sequence' +ARGUMENT EXTEND constr_comma_sequence' TYPED AS constr_list - PRINTED BY pr_constr_coma_sequence -| [ constr(c) "," constr_coma_sequence'(l) ] -> [ c::l ] + PRINTED BY pr_constr_comma_sequence +| [ constr(c) "," constr_comma_sequence'(l) ] -> [ c::l ] | [ constr(c) ] -> [ [c] ] END @@ -133,7 +137,7 @@ let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc ARGUMENT EXTEND auto_using' TYPED AS constr_list PRINTED BY pr_auto_using -| [ "using" constr_coma_sequence'(l) ] -> [ l ] +| [ "using" constr_comma_sequence'(l) ] -> [ l ] | [ ] -> [ [] ] END @@ -144,10 +148,10 @@ module Tactic = Pcoq.Tactic type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) = - Genarg.create_arg None "function_rec_definition_loc" + Genarg.create_arg "function_rec_definition_loc" let function_rec_definition_loc = - Pcoq.create_generic_entry "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) + Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) GEXTEND Gram GLOBAL: function_rec_definition_loc ; @@ -158,6 +162,11 @@ GEXTEND Gram END +let () = + let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in + let printer _ _ _ _ = str "<Unavailable printer for rec_definition>" in + Pptactic.declare_extra_genarg_pprule wit_function_rec_definition_loc raw_printer printer printer + (* TASSI: n'importe quoi ! *) VERNAC COMMAND EXTEND Function ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] @@ -186,18 +195,16 @@ END let warning_error names e = - let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in + let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> - Pp.msg_warning - (str "Cannot define graph(s) for " ++ - h 1 (pr_enum Libnames.pr_reference names) ++ - if do_observe () then (spc () ++ Errors.print e) else mt ()) + let names = pr_enum Libnames.pr_reference names in + let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in + warn_cannot_define_graph (names,error) | Defining_principle e -> - Pp.msg_warning - (str "Cannot define principle(s) for "++ - h 1 (pr_enum Libnames.pr_reference names) ++ - if do_observe () then Errors.print e else mt ()) + let names = pr_enum Libnames.pr_reference names in + let error = if do_observe () then CErrors.print e else mt () in + warn_cannot_define_principle (names,error) | _ -> raise e @@ -220,15 +227,15 @@ VERNAC COMMAND EXTEND NewFunctionalScheme ; try Functional_principles_types.build_scheme fas with Functional_principles_types.No_graph_found -> - Errors.error ("Cannot generate induction principle(s)") - | e when Errors.noncritical e -> + CErrors.error ("Cannot generate induction principle(s)") + | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in warning_error names e end | _ -> assert false (* we can only have non empty list *) end - | e when Errors.noncritical e -> + | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in warning_error names e end |