diff options
Diffstat (limited to 'plugins')
67 files changed, 140 insertions, 208 deletions
diff --git a/plugins/btauto/btauto_plugin.mllib b/plugins/btauto/btauto_plugin.mlpack index 319a9c302a..2410f906a3 100644 --- a/plugins/btauto/btauto_plugin.mllib +++ b/plugins/btauto/btauto_plugin.mlpack @@ -1,3 +1,2 @@ Refl_btauto G_btauto -Btauto_plugin_mod diff --git a/plugins/cc/cc_plugin.mllib b/plugins/cc/cc_plugin.mlpack index 1bcfc5378b..27e903fd38 100644 --- a/plugins/cc/cc_plugin.mllib +++ b/plugins/cc/cc_plugin.mlpack @@ -2,4 +2,3 @@ Ccalgo Ccproof Cctac G_congruence -Cc_plugin_mod diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 898dcd2551..76db2f3c2f 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -25,7 +25,7 @@ let init_size=5 let cc_verbose=ref false let debug x = - if !cc_verbose then msg_debug (x ()) + if !cc_verbose then Feedback.msg_debug (x ()) let _= let gdopt= diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index c8924073c7..bd788a425a 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -424,10 +424,10 @@ let cc_tactic depth additionnal_terms = List.map (build_term_to_complete uf newmeta) (epsilons uf) in - Pp.msg_info + Feedback.msg_info (Pp.str "Goal is solvable by congruence but \ some arguments are missing."); - Pp.msg_info + Feedback.msg_info (Pp.str " Try " ++ hov 8 begin diff --git a/plugins/decl_mode/decl_mode_plugin.mllib b/plugins/decl_mode/decl_mode_plugin.mlpack index 39342dbd1c..1b84a0790f 100644 --- a/plugins/decl_mode/decl_mode_plugin.mllib +++ b/plugins/decl_mode/decl_mode_plugin.mlpack @@ -3,4 +3,3 @@ Decl_interp Decl_proof_instr Ppdecl_proof G_decl_mode -Decl_mode_plugin_mod diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index be6ce59bd3..3fa600ac29 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -169,7 +169,7 @@ let do_daimon () = daimon_instr env p end in - if not status then Pp.feedback Feedback.AddedAxiom else () + if not status then Feedback.feedback Feedback.AddedAxiom else () (* post-instruction focus management *) @@ -291,7 +291,7 @@ let justification tac gls= error "Insufficient justification." else begin - msg_warning (str "Insufficient justification."); + Feedback.msg_warning (str "Insufficient justification."); daimon_tac gls end) gls @@ -1293,7 +1293,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = end; match bro with None -> - msg_warning (str "missing case"); + Feedback.msg_warning (str "missing case"); tacnext (mkMeta 1) | Some (sub_ids,tree) -> let br_args = diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 78a95143df..73d3d1bab8 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "decl_mode_plugin" + open Compat open Pp open Decl_expr @@ -98,7 +100,7 @@ let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr let classify_proof_instr = function | { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow - | _ -> VtProofStep false, VtLater + | _ -> Vernac_classifier.classify_as_proofstep (* We use the VERNAC EXTEND facility with a custom non-terminal to populate [proof_mode] with a new toplevel interpreter. diff --git a/plugins/derive/derive_plugin.mllib b/plugins/derive/derive_plugin.mlpack index 5ee0fc6da6..5ee0fc6da6 100644 --- a/plugins/derive/derive_plugin.mllib +++ b/plugins/derive/derive_plugin.mlpack diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 index 39cad4d03c..d4dc7e0eed 100644 --- a/plugins/derive/g_derive.ml4 +++ b/plugins/derive/g_derive.ml4 @@ -10,6 +10,8 @@ open Constrarg (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "derive_plugin" + let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 67c1c59017..a03be5743f 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -541,7 +541,7 @@ let print_structure_to_file (fn,si,mo) dry struc = (if dry then None else si); (* Print the buffer content via Coq standard formatter (ok with coqide). *) if not (Int.equal (Buffer.length buf) 0) then begin - Pp.msg_notice (str (Buffer.contents buf)); + Feedback.msg_notice (str (Buffer.contents buf)); Buffer.reset buf end @@ -635,7 +635,7 @@ let simple_extraction r = in let ans = flag ++ print_one_decl struc (modpath_of_r r) d in reset (); - Pp.msg_notice ans + Feedback.msg_notice ans | _ -> assert false diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 4072109c43..e40621965f 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -989,7 +989,10 @@ let extract_constant env kn cb = | (Info,TypeScheme) -> (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () - | Def c -> mk_typ (Mod_subst.force_constr c) + | Def c -> + (match cb.const_proj with + | None -> mk_typ (Mod_subst.force_constr c) + | Some pb -> mk_typ pb.proj_body) | OpaqueDef c -> add_opaque r; if access_opaque () then @@ -998,7 +1001,10 @@ let extract_constant env kn cb = | (Info,Default) -> (match cb.const_body with | Undef _ -> warn_info (); mk_ax () - | Def c -> mk_def (Mod_subst.force_constr c) + | Def c -> + (match cb.const_proj with + | None -> mk_def (Mod_subst.force_constr c) + | Some pb -> mk_def pb.proj_body) | OpaqueDef c -> add_opaque r; if access_opaque () then diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mlpack index ad32124347..9184f65017 100644 --- a/plugins/extraction/extraction_plugin.mllib +++ b/plugins/extraction/extraction_plugin.mlpack @@ -9,4 +9,3 @@ Scheme Json Extract_env G_extraction -Extraction_plugin_mod diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index eb2f022443..19fda4aead 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "extraction_plugin" + (* ML names *) open Genarg @@ -101,7 +103,7 @@ END VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY | [ "Print" "Extraction" "Inline" ] - -> [ msg_info (print_extraction_inline ()) ] + -> [Feedback. msg_info (print_extraction_inline ()) ] END VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF @@ -123,7 +125,7 @@ END VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY | [ "Print" "Extraction" "Blacklist" ] - -> [ msg_info (print_extraction_blacklist ()) ] + -> [ Feedback.msg_info (print_extraction_blacklist ()) ] END VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index f336941ee3..560fe5aea8 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -300,7 +300,7 @@ let warning_axioms () = if List.is_empty info_axioms then () else begin let s = if Int.equal (List.length info_axioms) 1 then "axiom" else "axioms" in - msg_warning + Feedback.msg_warning (str ("The following "^s^" must be realized in the extracted code:") ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms) ++ str "." ++ fnl ()) @@ -310,7 +310,7 @@ let warning_axioms () = else begin let s = if Int.equal (List.length log_axioms) 1 then "axiom was" else "axioms were" in - msg_warning + Feedback.msg_warning (str ("The following logical "^s^" encountered:") ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n") @@ -326,12 +326,12 @@ let warning_opaques accessed = else let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in if accessed then - msg_warning + Feedback.msg_warning (str "The extraction is currently set to bypass opacity,\n" ++ str "the following opaque constant bodies have been accessed :" ++ lst ++ str "." ++ fnl ()) else - msg_warning + Feedback.msg_warning (str "The extraction now honors the opacity constraints by default,\n" ++ str "the following opaque constants have been extracted as axioms :" ++ lst ++ str "." ++ fnl () ++ @@ -339,7 +339,7 @@ let warning_opaques accessed = ++ fnl ()) let warning_both_mod_and_cst q mp r = - msg_warning + Feedback.msg_warning (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++ str "do you mean module " ++ pr_long_mp mp ++ @@ -358,7 +358,7 @@ let check_inside_module () = err (str "You can't do that within a Module Type." ++ fnl () ++ str "Close it and try again.") else if Lib.is_module () then - msg_warning + Feedback.msg_warning (str "Extraction inside an opened module is experimental.\n" ++ str "In case of problem, close it first.\n") @@ -368,7 +368,7 @@ let check_inside_section () = str "Close it and try again.") let warning_id s = - msg_warning (str ("The identifier "^s^ + Feedback.msg_warning (str ("The identifier "^s^ " contains __ which is reserved for the extraction")) let error_constant r = @@ -449,7 +449,7 @@ let error_remaining_implicit k = let warning_remaining_implicit k = let s = msg_of_implicit k in - msg_warning + Feedback.msg_warning (str ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++ str "Extraction SafeImplicits is unset, extracting nonetheless," ++ fnl () ++ str "but this code is potentially unsafe, please review it manually.") @@ -465,7 +465,7 @@ let check_loaded_modfile mp = match base_mp mp with | _ -> () let info_file f = - Flags.if_verbose msg_info + Flags.if_verbose Feedback.msg_info (str ("The file "^f^" has been created by extraction.")) diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 134b6ba947..cec3505a97 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -74,7 +74,7 @@ END VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY | [ "Print" "Firstorder" "Solver" ] -> [ - Pp.msg_info + Feedback.msg_info (Pp.(++) (Pp.str"Firstorder solver tactic is ") (print_default_solver ())) ] END @@ -131,7 +131,7 @@ ARGUMENT EXTEND firstorder_using | [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ] | [ "using" reference(a) reference(b) reference_list(l) ] -> [ Flags.if_verbose - Pp.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator"); + Feedback.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator"); a::b::l ] | [ ] -> [ [] ] @@ -153,6 +153,8 @@ TACTIC EXTEND gintuition END open Proofview.Notations +open Cc_plugin +open Decl_mode_plugin let default_declarative_automation = Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *) diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 3b9f67f664..d7da85b4f4 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -32,7 +32,7 @@ let ground_tac solver startseq gl= update_flags (); let rec toptac skipped seq gl= if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 - then Pp.msg_debug (Printer.pr_goal gl); + then Feedback.msg_debug (Printer.pr_goal gl); tclORELSE (axiom_tac seq.gl seq) begin try diff --git a/plugins/firstorder/ground_plugin.mllib b/plugins/firstorder/ground_plugin.mlpack index 447a1fb513..65fb2e9a1d 100644 --- a/plugins/firstorder/ground_plugin.mllib +++ b/plugins/firstorder/ground_plugin.mlpack @@ -5,4 +5,3 @@ Rules Instances Ground G_ground -Ground_plugin_mod diff --git a/plugins/fourier/fourier_plugin.mllib b/plugins/fourier/fourier_plugin.mlpack index 0383b1a80b..b6262f8aeb 100644 --- a/plugins/fourier/fourier_plugin.mllib +++ b/plugins/fourier/fourier_plugin.mlpack @@ -1,4 +1,3 @@ Fourier FourierR G_fourier -Fourier_plugin_mod diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 879145c2fa..52094cf085 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -52,17 +52,17 @@ let rec print_debug_queue e = let _ = match e with | Some e -> - Pp.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) + Feedback.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) | None -> begin - Pp.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal); + Feedback.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal); end in print_debug_queue None ; end let observe strm = if do_observe () - then Pp.msg_debug strm + then Feedback.msg_debug strm else () let do_observe_tac s tac g = diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 91a826c731..5b4fb25955 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -19,7 +19,7 @@ exception Toberemoved let observe s = if do_observe () - then Pp.msg_debug s + then Feedback.msg_debug s (* Transform an inductive induction principle into diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 6dfc23511e..c63527deaf 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -193,12 +193,12 @@ let warning_error names e = let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> - Pp.msg_warning + Feedback.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 ()) | Defining_principle e -> - Pp.msg_warning + Feedback.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 ()) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 8a0a1a064d..c424fe1226 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -14,7 +14,7 @@ open Misctypes let observe strm = if do_observe () - then Pp.msg_debug strm + then Feedback.msg_debug strm else () (*let observennl strm = if do_observe () @@ -1217,7 +1217,7 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) if Array.for_all (fun l -> let (n',nt',is_defined') = List.nth l i in - Name.equal n n' && Notation_ops.eq_glob_constr nt nt' && (is_defined : bool) == is_defined') + Name.equal n n' && glob_constr_eq nt nt' && (is_defined : bool) == is_defined') rels_params then l := param::!l diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 84a4d910ef..0cacb003d8 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -267,12 +267,12 @@ let derive_inversion fix_names = lind; with e when Errors.noncritical e -> let e' = process_vernac_interp_error e in - msg_warning + Feedback.msg_warning (str "Cannot build inversion information" ++ if do_observe () then (fnl() ++ Errors.print e') else mt ()) with e when Errors.noncritical e -> let e' = process_vernac_interp_error e in - msg_warning + Feedback.msg_warning (str "Cannot build inversion information (early)" ++ if do_observe () then (fnl() ++ Errors.print e') else mt ()) @@ -292,12 +292,12 @@ let warning_error names e = in match e with | Building_graph e -> - Pp.msg_warning + Feedback.msg_warning (str "Cannot define graph(s) for " ++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ e_explain e) | Defining_principle e -> - Pp.msg_warning + Feedback.msg_warning (str "Cannot define principle(s) for "++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ e_explain e) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 72529fbbe3..94530bfde2 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -53,7 +53,7 @@ let pr_constr_with_binding prc (c,bl) : Pp.std_ppcmds = let observe strm = if do_observe () - then Pp.msg_debug strm + then Feedback.msg_debug strm else () (*let observennl strm = diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index c71d9a9ca4..99a165044c 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -504,19 +504,19 @@ let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in match c1 , c2 with | GApp(_,f1, arr1), GApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> - let _ = prstr "\nICI1!\n";Pp.flush_all() in + let _ = prstr "\nICI1!\n" in let args = filter_shift_stable lnk (arr1 @ arr2) in GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args) | GApp(_,f1, arr1), GApp(_,f2,arr2) -> raise NoMerge | GLetIn(_,nme,bdy,trm) , _ -> - let _ = prstr "\nICI2!\n";Pp.flush_all() in + let _ = prstr "\nICI2!\n" in let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in GLetIn(Loc.ghost,nme,bdy,newtrm) | _, GLetIn(_,nme,bdy,trm) -> - let _ = prstr "\nICI3!\n";Pp.flush_all() in + let _ = prstr "\nICI3!\n" in let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in GLetIn(Loc.ghost,nme,bdy,newtrm) - | _ -> let _ = prstr "\nICI4!\n";Pp.flush_all() in + | _ -> let _ = prstr "\nICI4!\n" in raise NoMerge let rec merge_app_unsafe c1 c2 shift filter_shift_stable = @@ -527,14 +527,14 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable = GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args) (* FIXME: what if the function appears in the body of the let? *) | GLetIn(_,nme,bdy,trm) , _ -> - let _ = prstr "\nICI2 '!\n";Pp.flush_all() in + let _ = prstr "\nICI2 '!\n" in let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in GLetIn(Loc.ghost,nme,bdy,newtrm) | _, GLetIn(_,nme,bdy,trm) -> - let _ = prstr "\nICI3 '!\n";Pp.flush_all() in + let _ = prstr "\nICI3 '!\n" in let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in GLetIn(Loc.ghost,nme,bdy,newtrm) - | _ -> let _ = prstr "\nICI4 '!\n";Pp.flush_all() in raise NoMerge + | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 10f08d3d13..95b4967faa 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -214,17 +214,17 @@ let print_debug_queue b e = begin let lmsg,goal = Stack.pop debug_queue in if b then - Pp.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) + Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) else begin - Pp.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal)); + Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal)); end; (* print_debug_queue false e; *) end let observe strm = if do_observe () - then Pp.msg_debug strm + then Feedback.msg_debug strm else () @@ -1529,7 +1529,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in - let _ = Table.extraction_inline true [Ident (Loc.ghost,term_id)] in + let _ = Extraction_plugin.Table.extraction_inline true [Ident (Loc.ghost,term_id)] in (* message "start second proof"; *) let stop = try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); @@ -1537,7 +1537,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num with e when Errors.noncritical e -> begin if do_observe () - then msg_debug (str "Cannot create equation Lemma " ++ Errors.print e) + then Feedback.msg_debug (str "Cannot create equation Lemma " ++ Errors.print e) else anomaly (Pp.str "Cannot create equation Lemma") ; true diff --git a/plugins/funind/recdef_plugin.mllib b/plugins/funind/recdef_plugin.mlpack index ec1f5436ca..2b443f2a1b 100644 --- a/plugins/funind/recdef_plugin.mllib +++ b/plugins/funind/recdef_plugin.mlpack @@ -8,4 +8,3 @@ Invfun Indfun Merge G_indfun -Recdef_plugin_mod diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 0fcfbfc711..e4aa1448eb 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -961,7 +961,7 @@ struct let parse_expr parse_constant parse_exp ops_spec env term = if debug - then Pp.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term); + then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term); (* let constant_or_variable env term = @@ -1082,7 +1082,7 @@ struct let rconstant term = if debug - then Pp.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ()); + then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ()); let res = rconstant term in if debug then (Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ; @@ -1122,7 +1122,7 @@ struct let parse_arith parse_op parse_expr env cstr gl = if debug - then Pp.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm cstr ++ fnl ()); + then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm cstr ++ fnl ()); match kind_of_term cstr with | App(op,args) -> let (op,lhs,rhs) = parse_op gl (op,args) in @@ -1651,12 +1651,12 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 if debug then begin - Pp.pp (Pp.str "Formula....\n") ; + Feedback.msg_notice (Pp.str "Formula....\n") ; let formula_typ = (Term.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in let ff = dump_formula formula_typ (dump_cstr spec.typ spec.dump_coeff) ff in - Pp.pp (Printer.prterm ff) ; Pp.pp_flush (); - Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff + Feedback.msg_notice (Printer.prterm ff); + Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff end; match witness_list_tags prover cnf_ff with @@ -1676,11 +1676,11 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 if debug then begin - Pp.pp (Pp.str "\nAFormula\n") ; + Feedback.msg_notice (Pp.str "\nAFormula\n") ; let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in let ff' = dump_formula formula_typ (dump_cstr spec.typ spec.dump_coeff) ff' in - Pp.pp (Printer.prterm ff') ; Pp.pp_flush (); + Feedback.msg_notice (Printer.prterm ff'); Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff' end; @@ -1733,7 +1733,7 @@ let micromega_gen with | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout") - | CsdpNotFound -> flush stdout ; Pp.pp_flush () ; + | CsdpNotFound -> flush stdout ; Tacticals.New.tclFAIL 0 (Pp.str (" Skipping what remains of this tactic: the complexity of the goal requires " ^ "the use of a specialized external tool called csdp. \n\n" @@ -1818,7 +1818,7 @@ let micromega_genr prover = with | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "TimeOut") | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") - | CsdpNotFound -> flush stdout ; Pp.pp_flush () ; + | CsdpNotFound -> Tacticals.New.tclFAIL 0 (Pp.str (" Skipping what remains of this tactic: the complexity of the goal requires " ^ "the use of a specialized external tool called csdp. \n\n" @@ -1903,7 +1903,7 @@ let call_csdpcert_q provername poly = let cert = Certificate.q_cert_of_pos cert in if Mc.qWeakChecker poly cert then Some cert - else ((print_string "buggy certificate" ; flush stdout) ;None) + else ((print_string "buggy certificate") ;None) let call_csdpcert_z provername poly = let l = List.map (fun (e,o) -> (z_to_q_pol e,o)) poly in diff --git a/plugins/micromega/micromega_plugin.mllib b/plugins/micromega/micromega_plugin.mlpack index f53a9e3797..ed253da3fd 100644 --- a/plugins/micromega/micromega_plugin.mllib +++ b/plugins/micromega/micromega_plugin.mlpack @@ -7,4 +7,3 @@ Certificate Persistent_cache Coq_micromega G_micromega -Micromega_plugin_mod diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 6a03e2d61f..88b13abf9a 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -212,9 +212,11 @@ let find t k = res let memo cache f = - let tbl = lazy (open_in cache) in - fun x -> - let tbl = Lazy.force tbl in + let tbl = lazy (try Some (open_in cache) with _ -> None) in + fun x -> + match Lazy.force tbl with + | None -> f x + | Some tbl -> try find tbl x with diff --git a/plugins/nsatz/nsatz_plugin.mllib b/plugins/nsatz/nsatz_plugin.mlpack index e991fb76f7..b55adf43c0 100644 --- a/plugins/nsatz/nsatz_plugin.mllib +++ b/plugins/nsatz/nsatz_plugin.mlpack @@ -3,4 +3,3 @@ Polynom Ideal Nsatz G_nsatz -Nsatz_plugin_mod diff --git a/plugins/omega/omega_plugin.mllib b/plugins/omega/omega_plugin.mlpack index 2b387fdcee..df7f1047f2 100644 --- a/plugins/omega/omega_plugin.mllib +++ b/plugins/omega/omega_plugin.mlpack @@ -1,4 +1,3 @@ Omega Coq_omega G_omega -Omega_plugin_mod diff --git a/plugins/plugins.itarget b/plugins/plugins.itarget deleted file mode 100644 index 56aa42b069..0000000000 --- a/plugins/plugins.itarget +++ /dev/null @@ -1,3 +0,0 @@ -pluginsopt.otarget -pluginsbyte.otarget -pluginsvo.otarget
\ No newline at end of file diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget deleted file mode 100644 index d8752f8b80..0000000000 --- a/plugins/pluginsbyte.itarget +++ /dev/null @@ -1,21 +0,0 @@ -btauto/btauto_plugin.cma -setoid_ring/newring_plugin.cma -extraction/extraction_plugin.cma -decl_mode/decl_mode_plugin.cma -firstorder/ground_plugin.cma -rtauto/rtauto_plugin.cma -fourier/fourier_plugin.cma -romega/romega_plugin.cma -omega/omega_plugin.cma -micromega/micromega_plugin.cma -cc/cc_plugin.cma -nsatz/nsatz_plugin.cma -funind/recdef_plugin.cma -syntax/ascii_syntax_plugin.cma -syntax/nat_syntax_plugin.cma -syntax/numbers_syntax_plugin.cma -syntax/r_syntax_plugin.cma -syntax/string_syntax_plugin.cma -syntax/z_syntax_plugin.cma -quote/quote_plugin.cma -derive/derive_plugin.cma
\ No newline at end of file diff --git a/plugins/pluginsdyn.itarget b/plugins/pluginsdyn.itarget deleted file mode 100644 index 220e5182d9..0000000000 --- a/plugins/pluginsdyn.itarget +++ /dev/null @@ -1,24 +0,0 @@ -btauto/btauto_plugin.cmxs -field/field_plugin.cmxs -setoid_ring/newring_plugin.cmxs -extraction/extraction_plugin.cmxs -decl_mode/decl_mode_plugin.cmxs -firstorder/ground_plugin.cmxs -rtauto/rtauto_plugin.cmxs -fourier/fourier_plugin.cmxs -romega/romega_plugin.cmxs -omega/omega_plugin.cmxs -micromega/micromega_plugin.cmxs -subtac/subtac_plugin.cmxs -ring/ring_plugin.cmxs -cc/cc_plugin.cmxs -nsatz/nsatz_plugin.cmxs -funind/recdef_plugin.cmxs -syntax/ascii_syntax_plugin.cmxs -syntax/nat_syntax_plugin.cmxs -syntax/numbers_syntax_plugin.cmxs -syntax/r_syntax_plugin.cmxs -syntax/string_syntax_plugin.cmxs -syntax/z_syntax_plugin.cmxs -quote/quote_plugin.cmxs -derive/derive_plugin.cmxs diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget deleted file mode 100644 index 04a1e711cb..0000000000 --- a/plugins/pluginsopt.itarget +++ /dev/null @@ -1,21 +0,0 @@ -btauto/btauto_plugin.cmxa -setoid_ring/newring_plugin.cmxa -extraction/extraction_plugin.cmxa -decl_mode/decl_mode_plugin.cmxa -firstorder/ground_plugin.cmxa -rtauto/rtauto_plugin.cmxa -fourier/fourier_plugin.cmxa -romega/romega_plugin.cmxa -omega/omega_plugin.cmxa -micromega/micromega_plugin.cmxa -cc/cc_plugin.cmxa -nsatz/nsatz_plugin.cmxa -funind/recdef_plugin.cmxa -syntax/ascii_syntax_plugin.cmxa -syntax/nat_syntax_plugin.cmxa -syntax/numbers_syntax_plugin.cmxa -syntax/r_syntax_plugin.cmxa -syntax/string_syntax_plugin.cmxa -syntax/z_syntax_plugin.cmxa -quote/quote_plugin.cmxa -derive/derive_plugin.cmxa diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget deleted file mode 100644 index a59bf29c98..0000000000 --- a/plugins/pluginsvo.itarget +++ /dev/null @@ -1,12 +0,0 @@ -btauto/vo.otarget -fourier/vo.otarget -funind/vo.otarget -nsatz/vo.otarget -micromega/vo.otarget -omega/vo.otarget -quote/vo.otarget -romega/vo.otarget -rtauto/vo.otarget -setoid_ring/vo.otarget -extraction/vo.otarget -derive/vo.otarget
\ No newline at end of file diff --git a/plugins/quote/quote_plugin.mllib b/plugins/quote/quote_plugin.mllib deleted file mode 100644 index d1b3ccbe1e..0000000000 --- a/plugins/quote/quote_plugin.mllib +++ /dev/null @@ -1,3 +0,0 @@ -Quote -G_quote -Quote_plugin_mod diff --git a/plugins/quote/quote_plugin.mlpack b/plugins/quote/quote_plugin.mlpack new file mode 100644 index 0000000000..2e9be09d8d --- /dev/null +++ b/plugins/quote/quote_plugin.mlpack @@ -0,0 +1,2 @@ +Quote +G_quote diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 36511386ac..5e43dfc42d 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -1074,16 +1074,19 @@ Qed. avait utilisé le test précédent et fait une elimination dessus. *) Ltac elim_eq_term t1 t2 := + let Aux := fresh "Aux" in pattern (eq_term t1 t2); apply bool_eq_ind; intro Aux; [ generalize (eq_term_true t1 t2 Aux); clear Aux | generalize (eq_term_false t1 t2 Aux); clear Aux ]. Ltac elim_beq t1 t2 := + let Aux := fresh "Aux" in pattern (beq t1 t2); apply bool_eq_ind; intro Aux; [ generalize (beq_true t1 t2 Aux); clear Aux | generalize (beq_false t1 t2 Aux); clear Aux ]. Ltac elim_bgt t1 t2 := + let Aux := fresh "Aux" in pattern (bgt t1 t2); apply bool_eq_ind; intro Aux; [ generalize (bgt_true t1 t2 Aux); clear Aux | generalize (bgt_false t1 t2 Aux); clear Aux ]. diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index dca46cbcf7..a059512d84 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -9,7 +9,7 @@ open Pp open Util open Const_omega -module OmegaSolver = Omega.MakeOmegaSolver (Bigint) +module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) open OmegaSolver (* \section{Useful functions and flags} *) @@ -172,7 +172,7 @@ let print_env_reification env = in let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in let term_info = str "ENVIRONMENT OF TERMS :" ++ fnl () ++ loop 'V' 0 env.terms in - msg_debug (prop_info ++ fnl () ++ term_info) + Feedback.msg_debug (prop_info ++ fnl () ++ term_info) (* \subsection{Gestion des environnements de variable pour Omega} *) (* generation d'identifiant d'equation pour Omega *) diff --git a/plugins/romega/romega_plugin.mllib b/plugins/romega/romega_plugin.mlpack index 1625009d06..38d0e94111 100644 --- a/plugins/romega/romega_plugin.mllib +++ b/plugins/romega/romega_plugin.mlpack @@ -1,4 +1,3 @@ Const_omega Refl_omega G_romega -Romega_plugin_mod diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 3ba92b9f22..f3eae5f501 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -547,7 +547,7 @@ let pp_info () = int s_info.created_branches ++ str " created" ++ fnl () ++ str "Hypotheses : " ++ int s_info.created_hyps ++ str " created" ++ fnl () in - msg_info + Feedback.msg_info ( str "Proof-search statistics :" ++ fnl () ++ count_info ++ str "Branch ends: " ++ diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 73dc13e72e..0a0b459156 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -276,7 +276,7 @@ let rtauto_tac gls= begin reset_info (); if !verbose then - msg_info (str "Starting proof-search ..."); + Feedback.msg_info (str "Starting proof-search ..."); end in let search_start_time = System.get_time () in let prf = @@ -286,10 +286,10 @@ let rtauto_tac gls= let search_end_time = System.get_time () in let _ = if !verbose then begin - msg_info (str "Proof tree found in " ++ + Feedback.msg_info (str "Proof tree found in " ++ System.fmt_time_difference search_start_time search_end_time); pp_info (); - msg_info (str "Building proof term ... ") + Feedback.msg_info (str "Building proof term ... ") end in let build_start_time=System.get_time () in let _ = step_count := 0; node_count := 0 in @@ -302,7 +302,7 @@ let rtauto_tac gls= let build_end_time=System.get_time () in let _ = if !verbose then begin - msg_info (str "Proof term built in " ++ + Feedback.msg_info (str "Proof term built in " ++ System.fmt_time_difference build_start_time build_end_time ++ fnl () ++ str "Proof size : " ++ int !step_count ++ @@ -319,9 +319,9 @@ let rtauto_tac gls= Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in let tac_end_time = System.get_time () in let _ = - if !check then msg_info (str "Proof term type-checking is on"); + if !check then Feedback.msg_info (str "Proof term type-checking is on"); if !verbose then - msg_info (str "Internal tactic executed in " ++ + Feedback.msg_info (str "Internal tactic executed in " ++ System.fmt_time_difference tac_start_time tac_end_time) in result diff --git a/plugins/rtauto/rtauto_plugin.mllib b/plugins/rtauto/rtauto_plugin.mlpack index 0e34604495..61c5e945bc 100644 --- a/plugins/rtauto/rtauto_plugin.mllib +++ b/plugins/rtauto/rtauto_plugin.mlpack @@ -1,4 +1,3 @@ Proof_search Refl_tauto G_rtauto -Rtauto_plugin_mod diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index f5a7340487..f64226e334 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -60,9 +60,9 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in add_theory id (ic t) set k cst (pre,post) power sign div] | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [ - msg_notice (strbrk "The following ring structures have been declared:"); + Feedback.msg_notice (strbrk "The following ring structures have been declared:"); Spmap.iter (fun fn fi -> - msg_notice (hov 2 + Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ str"with carrier "++ pr_constr fi.ring_carrier++spc()++ str"and equivalence relation "++ pr_constr fi.ring_req)) @@ -89,9 +89,9 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div] | [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [ - msg_notice (strbrk "The following field structures have been declared:"); + Feedback.msg_notice (strbrk "The following field structures have been declared:"); Spmap.iter (fun fn fi -> - msg_notice (hov 2 + Feedback.msg_notice (hov 2 (Ppconstr.pr_id (Libnames.basename fn)++spc()++ str"with carrier "++ pr_constr fi.field_carrier++spc()++ str"and equivalence relation "++ pr_constr fi.field_req)) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 271bf35a88..57ef920325 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -34,15 +34,6 @@ open Proofview.Notations (****************************************************************************) (* controlled reduction *) -(** ppedrot: something dubious here, we're obviously using evars the wrong - way. FIXME! *) - -let mark_arg i c = mkEvar(Evar.unsafe_of_int i,[|c|]) -let unmark_arg f c = - match destEvar c with - | (i,[|c|]) -> f (Evar.repr i) c - | _ -> assert false - type protect_flag = Eval|Prot|Rec let tag_arg tag_rec map subs i c = @@ -75,12 +66,10 @@ and mk_clos_app_but f_map subs f args n = let fargs, args' = Array.chop n args in let f' = mkApp(f,fargs) in match f_map (global_of_constr_nofail f') with - Some map -> - mk_clos_deep - (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s')) - subs - (mkApp (mark_arg (-1) f', Array.mapi mark_arg args')) - | None -> mk_clos_app_but f_map subs f args (n+1) + | Some map -> + let f i t = tag_arg (mk_clos_but f_map subs) map subs i t in + mk_red (FApp (f (-1) f', Array.mapi f args')) + | None -> mk_atom (mkApp (f, args)) let interp_map l t = try Some(List.assoc_f eq_gr t l) with Not_found -> None @@ -106,6 +95,7 @@ let protect_tac_in map id = (****************************************************************************) let closed_term t l = + let open Quote_plugin in let l = List.map Universes.constr_of_global l in let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in if Quote.closed_under cs t then tclIDTAC else tclFAIL 0 (mt()) @@ -527,7 +517,7 @@ let ring_equality env evd (r,add,mul,opp,req) = let op_morph = op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in Flags.if_verbose - msg_info + Feedback.msg_info (str"Using setoid \""++pr_constr req++str"\""++spc()++ str"and morphisms \""++pr_constr add_m_lem ++ str"\","++spc()++ str"\""++pr_constr mul_m_lem++ @@ -536,7 +526,7 @@ let ring_equality env evd (r,add,mul,opp,req) = op_morph) | None -> (Flags.if_verbose - msg_info + Feedback.msg_info (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++ str"and morphisms \""++pr_constr add_m_lem ++ str"\""++spc()++str"and \""++ diff --git a/plugins/setoid_ring/newring_plugin.mllib b/plugins/setoid_ring/newring_plugin.mllib deleted file mode 100644 index 7d6c495889..0000000000 --- a/plugins/setoid_ring/newring_plugin.mllib +++ /dev/null @@ -1,3 +0,0 @@ -Newring -Newring_plugin_mod -G_newring diff --git a/plugins/setoid_ring/newring_plugin.mlpack b/plugins/setoid_ring/newring_plugin.mlpack new file mode 100644 index 0000000000..23663b4090 --- /dev/null +++ b/plugins/setoid_ring/newring_plugin.mlpack @@ -0,0 +1,2 @@ +Newring +G_newring diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 67c9dd0a38..03b49e3336 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "ascii_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + open Pp open Errors open Util diff --git a/plugins/syntax/ascii_syntax_plugin.mllib b/plugins/syntax/ascii_syntax_plugin.mllib deleted file mode 100644 index b00f92506e..0000000000 --- a/plugins/syntax/ascii_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Ascii_syntax -Ascii_syntax_plugin_mod diff --git a/plugins/syntax/ascii_syntax_plugin.mlpack b/plugins/syntax/ascii_syntax_plugin.mlpack new file mode 100644 index 0000000000..7b9213a0e2 --- /dev/null +++ b/plugins/syntax/ascii_syntax_plugin.mlpack @@ -0,0 +1 @@ +Ascii_syntax diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 5f44904c3c..3142c8cf00 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "nat_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + (* This file defines the printer for natural numbers in [nat] *) (*i*) @@ -25,7 +29,7 @@ let threshold = of_int 5000 let nat_of_int dloc n = if is_pos_or_zero n then begin if less_than threshold n then - msg_warning + Feedback.msg_warning (strbrk "Stack overflow or segmentation fault happens when " ++ strbrk "working with large numbers in nat (observed threshold " ++ strbrk "may vary from 5000 to 70000 depending on your system " ++ diff --git a/plugins/syntax/nat_syntax_plugin.mllib b/plugins/syntax/nat_syntax_plugin.mllib deleted file mode 100644 index 69b0cb20f6..0000000000 --- a/plugins/syntax/nat_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Nat_syntax -Nat_syntax_plugin_mod diff --git a/plugins/syntax/nat_syntax_plugin.mlpack b/plugins/syntax/nat_syntax_plugin.mlpack new file mode 100644 index 0000000000..39bdd62f47 --- /dev/null +++ b/plugins/syntax/nat_syntax_plugin.mlpack @@ -0,0 +1 @@ +Nat_syntax diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index fe9f1319eb..57cb2f897a 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "numbers_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + (* digit-based syntax for int31, bigN bigZ and bigQ *) open Bigint @@ -180,7 +184,7 @@ let bigN_of_pos_bigint dloc n = let word = word_of_pos_bigint dloc h n in let args = if h < n_inlined then [word] - else [Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word] + else [Nat_syntax_plugin.Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word] in GApp (dloc, ref_constructor, args) diff --git a/plugins/syntax/numbers_syntax_plugin.mllib b/plugins/syntax/numbers_syntax_plugin.mllib deleted file mode 100644 index ebc0bb2022..0000000000 --- a/plugins/syntax/numbers_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Numbers_syntax -Numbers_syntax_plugin_mod diff --git a/plugins/syntax/numbers_syntax_plugin.mlpack b/plugins/syntax/numbers_syntax_plugin.mlpack new file mode 100644 index 0000000000..e48c00a0d0 --- /dev/null +++ b/plugins/syntax/numbers_syntax_plugin.mlpack @@ -0,0 +1 @@ +Numbers_syntax diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 05d73f9ec1..3ae2d45f32 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -10,6 +10,10 @@ open Util open Names open Globnames +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "r_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + exception Non_closed_number (**********************************************************************) diff --git a/plugins/syntax/r_syntax_plugin.mllib b/plugins/syntax/r_syntax_plugin.mllib deleted file mode 100644 index 5c173a140f..0000000000 --- a/plugins/syntax/r_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -R_syntax -R_syntax_plugin_mod diff --git a/plugins/syntax/r_syntax_plugin.mlpack b/plugins/syntax/r_syntax_plugin.mlpack new file mode 100644 index 0000000000..d4ee75ea48 --- /dev/null +++ b/plugins/syntax/r_syntax_plugin.mlpack @@ -0,0 +1 @@ +R_syntax diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index 2e696f391f..de0fa77eff 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -7,10 +7,14 @@ (***********************************************************************) open Globnames -open Ascii_syntax +open Ascii_syntax_plugin.Ascii_syntax open Glob_term open Coqlib +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "string_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + exception Non_closed_string (* make a string term from the string s *) diff --git a/plugins/syntax/string_syntax_plugin.mllib b/plugins/syntax/string_syntax_plugin.mllib deleted file mode 100644 index b108c9e007..0000000000 --- a/plugins/syntax/string_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -String_syntax -String_syntax_plugin_mod diff --git a/plugins/syntax/string_syntax_plugin.mlpack b/plugins/syntax/string_syntax_plugin.mlpack new file mode 100644 index 0000000000..45d6e0fa23 --- /dev/null +++ b/plugins/syntax/string_syntax_plugin.mlpack @@ -0,0 +1 @@ +String_syntax diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 53c1b5d7a0..ce86c0a65f 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -12,6 +12,10 @@ open Util open Names open Bigint +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "z_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + exception Non_closed_number (**********************************************************************) diff --git a/plugins/syntax/z_syntax_plugin.mllib b/plugins/syntax/z_syntax_plugin.mllib deleted file mode 100644 index 36d41acc20..0000000000 --- a/plugins/syntax/z_syntax_plugin.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Z_syntax -Z_syntax_plugin_mod diff --git a/plugins/syntax/z_syntax_plugin.mlpack b/plugins/syntax/z_syntax_plugin.mlpack new file mode 100644 index 0000000000..411260c04c --- /dev/null +++ b/plugins/syntax/z_syntax_plugin.mlpack @@ -0,0 +1 @@ +Z_syntax |