diff options
65 files changed, 331 insertions, 397 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 2a325f2d71..698452cb2b 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -1,10 +1,17 @@ # This file describes the maintainers for the main components. See # `dev/doc/MERGING.md`. -########## GitHub metadata, including this file ########## +########## Contributing process ########## -/.github/ @maximedenes -# Secondary maintainer @Zimmi48 +/.github/ @coq/contributing-process-maintainers + +/CONTRIBUTING.md @coq/contributing-process-maintainers + +/dev/doc/release-process.md @coq/contributing-process-maintainers + +/dev/doc/MERGING.md @coq/pushers +# This ensures that all members of the @coq/pushers +# team are notified when the merging doc changes. ########## Build system ########## @@ -45,19 +52,12 @@ azure-pipelines.yml @coq/ci-maintainers /INSTALL* @Zimmi48 # Secondary maintainer @maximedenes -/CONTRIBUTING.md @Zimmi48 -# Secondary maintainer @maximedenes - /CODE_OF_CONDUCT.md @Zimmi48 # Secondary maintainer @mattam82 /dev/doc/ @Zimmi48 # Secondary maintainer @maximedenes -/dev/doc/MERGING.md @coq/pushers -# This ensures that all members of the @coq/pushers -# team are notified when the merging doc changes. - /dev/doc/changes.md @ghost # Trick to avoid getting review requests # each time someone modifies the dev changelog diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 529a912bb6..cbead97529 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -21,6 +21,7 @@ well. - [Support](#support) - [Standard libraries](#standard-libraries) - [Maintaining existing packages in coq-community](#maintaining-existing-packages-in-coq-community) + - [Contributing to the editor support packages](#contributing-to-the-editor-support-packages) - [Contributing to the website or the package archive](#contributing-to-the-website-or-the-package-archive) - [Other ways of creating content](#other-ways-of-creating-content) - [Issues](#issues) @@ -208,6 +209,10 @@ manifesto's README][coq-community-manifesto]. ### Contributing to the editor support packages ### +Besides CoqIDE, whose sources are available in this repository, and to +which you are welcome to contribute, there are a number of alternative +user interfaces for Coq, more often as an editor support package. + Here are the URLs of the repositories of the various editor support packages: @@ -216,6 +221,11 @@ packages: - Coqtail (Vim) <https://github.com/whonore/Coqtail> - VsCoq Reloaded (VsCode) <https://github.com/coq-community/vscoq> +And here are alternative user interfaces to be run in the web browser: + +- JsCoq (Coq executed in your browser) <https://github.com/ejgallego/jscoq> +- Jupyter kernel for Coq <https://github.com/EugeneLoy/coq_jupyter/> + Each of them has their own contribution process. ### Contributing to the website or the package archive ### @@ -616,8 +626,26 @@ documentation][coqdoc-documentation] to learn more. ### Fixing bugs and performing small changes ### -Just open a PR with your fix. If it is not yet completed, do not -hesitate to open a [*draft PR*][GitHub-draft-PR] to get early +Before fixing a bug, it is best to check that it was reported before: + +- If it was already reported and you intend to fix it, self-assign the + issue (if you have the permission), or leave a comment marking your + intention to work on it (and a contributor with write-access may + then assign the issue to you). + +- If the issue already has an assignee, you should check with them if + they still intend to work on it. If the assignment is several + weeks, months, or even years (!) old, there are good chances that it + does not reflect their current priorities. + +- If the bug has not been reported before, it can be a good idea to + open an issue about it, while stating that you are preparing a fix. + The issue can be the place to discuss about the bug itself while the + PR will be the place to discuss your proposed fix. + +In any case, feel free to just ignore the recommendation above, and +jump ahead and open a PR with your fix. If it is not yet complete, do +not hesitate to open a [*draft PR*][GitHub-draft-PR] to get early feedback, and talk to developers on [Gitter][]. It is generally a good idea to add a regression test to the @@ -638,12 +666,12 @@ merged. So it is recommended that before spending a lot of time coding, you seek feedback from maintainers to see if your change would be -supported, and if they have recommendation about its implementation. +supported, and if they have recommendations about its implementation. You can do this informally by opening an issue, or more formally by producing a design document as a [Coq Enhancement Proposal][CEP]. Another recommendation is that you do not put several unrelated -changes (even if you produced them together) in the same PR. In +changes in the same PR (even if you produced them together). In particular, make sure you split bug fixes into separate PRs when this is possible. More generally, smaller-sized PRs, or PRs changing less components, are more likely to be reviewed and merged promptly. diff --git a/Makefile.build b/Makefile.build index d1ed9a6f96..610af5fe40 100644 --- a/Makefile.build +++ b/Makefile.build @@ -396,9 +396,8 @@ doc_gram_rsts: doc/tools/docgram/orderedGrammar ########################################################################### # Specific rules for Uint63 ########################################################################### -kernel/uint63.ml: kernel/write_uint63.ml kernel/uint63_i386_31.ml kernel/uint63_amd64_63.ml - $(SHOW)'WRITE $@' - $(HIDE)(cd kernel && ocaml unix.cma $(shell basename $<)) +kernel/uint63.ml: kernel/uint63_$(OCAML_INT_SIZE).ml + rm -f $@ && cp $< $@ && chmod a-w $@ ########################################################################### # Main targets (coqtop.opt, coqtop.byte) @@ -642,12 +641,6 @@ gramlib/.pack/gramlib__G%: gramlib/g% | gramlib/.pack # Specific rules for gramlib to pack it Dune / OCaml 4.08 style GRAMOBJS=$(addsuffix .cmo, $(GRAMFILES)) -gramlib/.pack/%: COND_BYTEFLAGS+=-no-alias-deps -w -49 -gramlib/.pack/%: COND_OPTFLAGS+=-no-alias-deps -w -49 - -gramlib/.pack/gramlib.%: COND_OPENFLAGS= -gramlib/.pack/gramlib__%: COND_OPENFLAGS=-open Gramlib - gramlib/.pack/gramlib.cma: $(GRAMOBJS) gramlib/.pack/gramlib.cmo $(SHOW)'OCAMLC -a -o $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $^ @@ -701,14 +694,15 @@ kernel/kernel.cmxa: kernel/kernel.mllib COND_IDEFLAGS=$(if $(filter ide/fake_ide% tools/coq_makefile%,$<), -I ide -I ide/protocol,) COND_PRINTERFLAGS=$(if $(filter dev/%,$<), -I dev,) -# For module packing -COND_OPENFLAGS= +COND_GRAMFLAGS=$(if $(filter gramlib/.pack/%,$<),-no-alias-deps -w -49,) $(if $(filter gramlib/.pack/gramlib__%,$<),-open Gramlib,) + +COND_KERFLAGS=$(if $(filter kernel/%,$<),-w +a-4-44-50,) COND_BYTEFLAGS= \ - $(COND_IDEFLAGS) $(COND_PRINTERFLAGS) $(MLINCLUDES) $(BYTEFLAGS) $(COND_OPENFLAGS) + $(COND_IDEFLAGS) $(COND_PRINTERFLAGS) $(MLINCLUDES) $(BYTEFLAGS) $(COND_GRAMFLAGS) $(COND_KERFLAGS) COND_OPTFLAGS= \ - $(COND_IDEFLAGS) $(MLINCLUDES) $(OPTFLAGS) $(COND_OPENFLAGS) + $(COND_IDEFLAGS) $(MLINCLUDES) $(OPTFLAGS) $(COND_GRAMFLAGS) $(COND_KERFLAGS) plugins/micromega/%.cmi: plugins/micromega/%.mli $(SHOW)'OCAMLC $<' @@ -718,8 +712,6 @@ plugins/nsatz/%.cmi: plugins/nsatz/%.mli $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< -kernel/%.cmi: COND_BYTEFLAGS+=-w +a-4-44-50 - %.cmi: %.mli $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< @@ -732,8 +724,6 @@ plugins/nsatz/%.cmo: plugins/nsatz/%.ml $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< -kernel/%.cmo: COND_BYTEFLAGS+=-w +a-4-44-50 - %.cmo: %.ml $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< @@ -783,8 +773,6 @@ user-contrib/%.cmx: user-contrib/%.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $< -kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50 - %.cmx: %.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $< diff --git a/Makefile.ide b/Makefile.ide index cb026cdf43..0a11f83a18 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -121,7 +121,7 @@ $(COQIDEBYTE): $(LINKIDE) ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile @rm -f $@ cp $< $@ - @chmod -w $@ + @chmod a-w $@ ide/%.cmi: ide/%.mli $(SHOW)'OCAMLC $<' diff --git a/configure.ml b/configure.ml index 3ced82718e..cef4faaf1a 100644 --- a/configure.ml +++ b/configure.ml @@ -1141,6 +1141,7 @@ let write_makefile f = pr "# Your architecture\n"; pr "# Can be obtain by UNIX command arch\n"; pr "ARCH=%s\n" arch; + pr "OCAML_INT_SIZE:=%d\n" Sys.int_size; pr "HASNATDYNLINK=%s\n\n" natdynlinkflag; pr "# Supplementary libs for some systems, currently:\n"; pr "# . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket\n"; diff --git a/dev/ci/user-overlays/10660-ejgallego-errors+private.sh b/dev/ci/user-overlays/10660-ejgallego-errors+private.sh new file mode 100644 index 0000000000..21ff60493b --- /dev/null +++ b/dev/ci/user-overlays/10660-ejgallego-errors+private.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10660" ] || [ "$CI_BRANCH" = "errors+private" ]; then + + coqhammer_CI_REF=errors+private + coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer + +fi diff --git a/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh new file mode 100644 index 0000000000..6dc44aa627 --- /dev/null +++ b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10674" ] || [ "$CI_BRANCH" = "proofs+declare_unif" ]; then + + equations_CI_REF=proofs+declare_unif + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index 7c06bb59f1..e3a5676942 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -30,7 +30,7 @@ exception Exception of exn (** This exception is used to signal abortion in [timeout] functions. *) -exception Timeout +exception Tac_Timeout (** This exception is used by the tactics to signal failure by lack of successes, rather than some other exceptions (like system @@ -38,7 +38,6 @@ exception Timeout exception TacticFailure of exn let _ = CErrors.register_handler begin function - | Timeout -> CErrors.user_err ~hdr:"Some timeout function" (Pp.str"Timeout!") | Exception e -> CErrors.print e | TacticFailure e -> CErrors.print e | _ -> raise CErrors.Unhandled @@ -99,7 +98,7 @@ struct let print_char = fun c -> (); fun () -> print_char c let timeout = fun n t -> (); fun () -> - Control.timeout n t () (Exception Timeout) + Control.timeout n t () (Exception Tac_Timeout) let make f = (); fun () -> try f () diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index 90c920439a..75920455ce 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -30,7 +30,7 @@ exception Exception of exn (** This exception is used to signal abortion in [timeout] functions. *) -exception Timeout +exception Tac_Timeout (** This exception is used by the tactics to signal failure by lack of successes, rather than some other exceptions (like system diff --git a/engine/proofview.ml b/engine/proofview.ml index 1fbad25d46..1f076470c1 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -907,11 +907,10 @@ let tclPROGRESS t = if not test then tclUNIT res else - tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) + tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress.")) -exception Timeout let _ = CErrors.register_handler begin function - | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") + | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") | _ -> raise CErrors.Unhandled end @@ -936,7 +935,8 @@ let tclTIMEOUT n t = end begin let open Logic_monad.NonLogical in function (e, info) -> match e with - | Logic_monad.Timeout -> return (Util.Inr (Timeout, info)) + | Logic_monad.Tac_Timeout -> + return (Util.Inr (Logic_monad.Tac_Timeout, info)) | Logic_monad.TacticFailure e -> return (Util.Inr (e, info)) | e -> Logic_monad.NonLogical.raise ~info e diff --git a/engine/proofview.mli b/engine/proofview.mli index d6ca94e405..764a4a0058 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -415,8 +415,6 @@ end (** Checks for interrupts *) val tclCHECKINTERRUPT : unit tactic -exception Timeout - (** [tclTIMEOUT n t] can have only one success. In case of timeout if fails with [tclZERO Timeout]. *) val tclTIMEOUT : int -> 'a tactic -> 'a tactic diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index f86cb0f6f2..ff0b90dcff 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -10,6 +10,9 @@ open Util module type GLexerType = Plexing.Lexer +type ty_norec = TyNoRec +type ty_mayrec = TyMayRec + module type S = sig type te @@ -27,8 +30,6 @@ module type S = val parse_token_stream : 'a e -> te Stream.t -> 'a val print : Format.formatter -> 'a e -> unit end - type ty_norec = TyNoRec - type ty_mayrec = TyMayRec type ('self, 'trec, 'a) ty_symbol type ('self, 'trec, 'f, 'r) ty_rule type 'a ty_rules @@ -92,9 +93,6 @@ let tokens con = egram.gtokens; !list -type ty_norec = TyNoRec -type ty_mayrec = TyMayRec - type ('a, 'b, 'c) ty_and_rec = | NoRec2 : (ty_norec, ty_norec, ty_norec) ty_and_rec | MayRec2 : ('a, 'b, ty_mayrec) ty_and_rec diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 658baf1de9..9e48460206 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -19,6 +19,9 @@ module type GLexerType = Plexing.Lexer (** The input signature for the functor [Grammar.GMake]: [te] is the type of the tokens. *) +type ty_norec = TyNoRec +type ty_mayrec = TyMayRec + module type S = sig type te @@ -36,8 +39,6 @@ module type S = val parse_token_stream : 'a e -> te Stream.t -> 'a val print : Format.formatter -> 'a e -> unit end - type ty_norec = TyNoRec - type ty_mayrec = TyMayRec type ('self, 'trec, 'a) ty_symbol type ('self, 'trec, 'f, 'r) ty_rule type 'a ty_rules diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 8d6a266c30..41d1da9694 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -20,31 +20,21 @@ let open_glob_file f = let close_glob_file () = close_out !glob_file -type glob_output_t = - | NoGlob - | StdOut - | MultFiles - | Feedback - | File of string +type glob_output = + | NoGlob + | Feedback + | MultFiles + | File of string let glob_output = ref NoGlob -let dump () = !glob_output != NoGlob +let dump () = !glob_output <> NoGlob -let noglob () = glob_output := NoGlob - -let dump_to_dotglob () = glob_output := MultFiles - -let dump_into_file f = - if String.equal f "stdout" then - (glob_output := StdOut; glob_file := stdout) - else - (glob_output := File f; open_glob_file f) - -let feedback_glob () = glob_output := Feedback +let set_glob_output mode = + glob_output := mode let dump_string s = - if dump () && !glob_output != Feedback then + if dump () && !glob_output != Feedback then output_string !glob_file s let start_dump_glob ~vfile ~vofile = @@ -57,13 +47,13 @@ let start_dump_glob ~vfile ~vofile = | File f -> open_glob_file f; output_string !glob_file "DIGEST NO\n" - | NoGlob | Feedback | StdOut -> + | NoGlob | Feedback -> () let end_dump_glob () = match !glob_output with | MultFiles | File _ -> close_glob_file () - | NoGlob | Feedback | StdOut -> () + | NoGlob | Feedback -> () let previous_state = ref MultFiles let pause () = previous_state := !glob_output; glob_output := NoGlob diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 60d62a1cb2..2b6a116a01 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -8,19 +8,19 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val open_glob_file : string -> unit -val close_glob_file : unit -> unit - val start_dump_glob : vfile:string -> vofile:string -> unit val end_dump_glob : unit -> unit val dump : unit -> bool -val noglob : unit -> unit -val dump_into_file : string -> unit (** special handling of "stdout" *) +type glob_output = + | NoGlob + | Feedback + | MultFiles (* one glob file per .v file *) + | File of string (* Single file for all coqc arguments *) -val dump_to_dotglob : unit -> unit -val feedback_glob : unit -> unit +(* Default "NoGlob" *) +val set_glob_output : glob_output -> unit val pause : unit -> unit val continue : unit -> unit diff --git a/kernel/dune b/kernel/dune index 4038bf5638..5f7502ef6b 100644 --- a/kernel/dune +++ b/kernel/dune @@ -3,7 +3,7 @@ (synopsis "The Coq Kernel") (public_name coq.kernel) (wrapped false) - (modules (:standard \ genOpcodeFiles uint63_i386_31 uint63_amd64_63 write_uint63)) + (modules (:standard \ genOpcodeFiles uint63_31 uint63_63)) (libraries lib byterun dynlink)) (executable @@ -16,7 +16,7 @@ (rule (targets uint63.ml) - (deps (:gen-file uint63_%{ocaml-config:architecture}_%{ocaml-config:int_size}.ml)) + (deps (:gen-file uint63_%{ocaml-config:int_size}.ml)) (action (copy# %{gen-file} %{targets}))) (documentation diff --git a/kernel/uint63.mli b/kernel/uint63.mli index 5542716af2..d22ba3468f 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + type t val uint_size : int diff --git a/kernel/uint63_i386_31.ml b/kernel/uint63_31.ml index b8eccd19fb..b8eccd19fb 100644 --- a/kernel/uint63_i386_31.ml +++ b/kernel/uint63_31.ml diff --git a/kernel/uint63_amd64_63.ml b/kernel/uint63_63.ml index 5c4028e1c8..5c4028e1c8 100644 --- a/kernel/uint63_amd64_63.ml +++ b/kernel/uint63_63.ml diff --git a/kernel/write_uint63.ml b/kernel/write_uint63.ml deleted file mode 100644 index 57a170c8f5..0000000000 --- a/kernel/write_uint63.ml +++ /dev/null @@ -1,38 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Equivalent of rm -f *) -let safe_remove f = - try Unix.chmod f 0o644; Sys.remove f with _ -> () - -(** * Generate an implementation of 63-bit arithmetic *) -let ml_file_copy input output = - safe_remove output; - let i = open_in input in - let o = open_out output in - let pr s = Printf.fprintf o s in - pr "(* DO NOT EDIT THIS FILE: automatically generated by ./write_uint63.ml *)\n"; - pr "(* see uint63_amd64.ml and uint63_x86.ml *)\n"; - try - while true do - output_string o (input_line i); output_char o '\n' - done - with End_of_file -> - close_in i; - close_out o; - Unix.chmod output 0o444 - -let write_uint63 () = - ml_file_copy - (if max_int = 1073741823 (* 32-bits *) then "uint63_i386_31.ml" - else (* 64 bits *) "uint63_amd64_63.ml") - "uint63.ml" - -let () = write_uint63 () diff --git a/lib/aux_file.mli b/lib/aux_file.mli index 60c8fb4449..b241fdc6cc 100644 --- a/lib/aux_file.mli +++ b/lib/aux_file.mli @@ -21,7 +21,7 @@ val contents : aux_file -> string M.t H.t val aux_file_name_for : string -> string val start_aux_file : aux_file:string -> v_file:string -> unit -val stop_aux_file : unit -> unit +val stop_aux_file : unit -> unit val recording : unit -> bool val record_in_aux_at : ?loc:Loc.t -> string -> string -> unit diff --git a/lib/flags.ml b/lib/flags.ml index 190de5853d..f09dc48f5d 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -41,8 +41,6 @@ let with_options ol f x = let () = List.iter2 (:=) ol vl in Exninfo.iraise reraise -let record_aux_file = ref false - let async_proofs_worker_id = ref "master" let async_proofs_is_worker () = !async_proofs_worker_id <> "master" diff --git a/lib/flags.mli b/lib/flags.mli index 1c96796220..185a5f8425 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -31,10 +31,6 @@ (** Command-line flags *) -(** Set by coqtop to tell the kernel to output to the aux file; will - be eventually removed by cleanups such as PR#1103 *) -val record_aux_file : bool ref - (** Async-related flags *) val async_proofs_worker_id : string ref val async_proofs_is_worker : unit -> bool diff --git a/parsing/extend.ml b/parsing/extend.ml index 63e121c0d1..ed6ebe5aed 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -79,8 +79,10 @@ type ('a,'b,'c) ty_user_symbol = (** {5 Type-safe grammar extension} *) -type norec = NoRec (* just two *) -type mayrec = MayRec (* incompatible types *) +(* Should be merged with gramlib's implementation *) + +type norec = Gramlib.Grammar.ty_norec +type mayrec = Gramlib.Grammar.ty_mayrec type ('self, 'trec, 'a) symbol = | Atoken : 'c Tok.p -> ('self, norec, 'c) symbol @@ -107,15 +109,3 @@ and 'a rules = type 'a production_rule = | Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule - -type 'a single_extend_statement = - string option * - (* Level *) - Gramlib.Gramext.g_assoc option * - (* Associativity *) - 'a production_rule list - (* Symbol list with the interpretation function *) - -type 'a extend_statement = - Gramlib.Gramext.position option * - 'a single_extend_statement list diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 3aaba27579..e0d63a723e 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -131,73 +131,57 @@ end (** Binding general entry keys to symbol *) -type ('s, 'trec, 'a, 'r) casted_rule = -| CastedRNo : ('s, G.ty_norec, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, norec, 'a, 'r) casted_rule -| CastedRMay : ('s, G.ty_mayrec, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, mayrec, 'a, 'r) casted_rule - -type ('s, 'trec, 'a) casted_symbol = -| CastedSNo : ('s, G.ty_norec, 'a) G.ty_symbol -> ('s, norec, 'a) casted_symbol -| CastedSMay : ('s, G.ty_mayrec, 'a) G.ty_symbol -> ('s, mayrec, 'a) casted_symbol - -let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) casted_symbol = +let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) G.ty_symbol = function -| Atoken t -> CastedSNo (G.s_token t) +| Atoken t -> G.s_token t | Alist1 s -> - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_list1 s) - | CastedSMay s -> CastedSMay (G.s_list1 s) end + let s = symbol_of_prod_entry_key s in + G.s_list1 s | Alist1sep (s,sep) -> - let CastedSNo sep = symbol_of_prod_entry_key sep in - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_list1sep s sep false) - | CastedSMay s -> CastedSMay (G.s_list1sep s sep false) end + let s = symbol_of_prod_entry_key s in + let sep = symbol_of_prod_entry_key sep in + G.s_list1sep s sep false | Alist0 s -> - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_list0 s) - | CastedSMay s -> CastedSMay (G.s_list0 s) end + let s = symbol_of_prod_entry_key s in + G.s_list0 s | Alist0sep (s,sep) -> - let CastedSNo sep = symbol_of_prod_entry_key sep in - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_list0sep s sep false) - | CastedSMay s -> CastedSMay (G.s_list0sep s sep false) end + let s = symbol_of_prod_entry_key s in + let sep = symbol_of_prod_entry_key sep in + G.s_list0sep s sep false | Aopt s -> - begin match symbol_of_prod_entry_key s with - | CastedSNo s -> CastedSNo (G.s_opt s) - | CastedSMay s -> CastedSMay (G.s_opt s) end -| Aself -> CastedSMay G.s_self -| Anext -> CastedSMay G.s_next -| Aentry e -> CastedSNo (G.s_nterm e) -| Aentryl (e, n) -> CastedSNo (G.s_nterml e n) + let s = symbol_of_prod_entry_key s in + G.s_opt s +| Aself -> G.s_self +| Anext -> G.s_next +| Aentry e -> G.s_nterm e +| Aentryl (e, n) -> G.s_nterml e n | Arules rs -> let warning msg = Feedback.msg_warning Pp.(str msg) in - CastedSNo (G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs)) + G.s_rules ~warning:(Some warning) (List.map symbol_of_rules rs) -and symbol_of_rule : type s tr a r. (s, tr, a, Loc.t -> r) Extend.rule -> (s, tr, a, Loc.t -> r) casted_rule = function -| Stop -> CastedRNo (G.r_stop, fun act loc -> act loc) +and symbol_of_rule : type s tr a r. (s, tr, a, Loc.t -> r) Extend.rule -> (s, tr, a, Loc.t -> r) G.ty_rule = function +| Stop -> + G.r_stop | Next (r, s) -> - begin match symbol_of_rule r, symbol_of_prod_entry_key s with - | CastedRNo (r, cast), CastedSNo s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) - | CastedRNo (r, cast), CastedSMay s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) - | CastedRMay (r, cast), CastedSNo s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) - | CastedRMay (r, cast), CastedSMay s -> CastedRMay (G.r_next r s, (fun act x -> cast (act x))) end + let r = symbol_of_rule r in + let s = symbol_of_prod_entry_key s in + G.r_next r s | NextNoRec (r, s) -> - let CastedRNo (r, cast) = symbol_of_rule r in - let CastedSNo s = symbol_of_prod_entry_key s in - CastedRNo (G.r_next_norec r s, (fun act x -> cast (act x))) + let r = symbol_of_rule r in + let s = symbol_of_prod_entry_key s in + G.r_next_norec r s and symbol_of_rules : type a. a Extend.rules -> a G.ty_rules = function | Rules (r, act) -> - let CastedRNo (symb, cast) = symbol_of_rule r in - G.rules (symb, cast act) + let symb = symbol_of_rule r in + G.rules (symb,act) (** FIXME: This is a hack around a deficient camlp5 API *) type 'a any_production = AnyProduction : ('a, 'tr, 'f, Loc.t -> 'a) G.ty_rule * 'f -> 'a any_production let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function | Rule (toks, act) -> - match symbol_of_rule toks with - | CastedRNo (symb, cast) -> AnyProduction (symb, cast act) - | CastedRMay (symb, cast) -> AnyProduction (symb, cast act) + AnyProduction (symbol_of_rule toks, act) let of_coq_single_extend_statement (lvl, assoc, rule) = (lvl, assoc, List.map of_coq_production_rule rule) @@ -215,6 +199,18 @@ let fix_extend_statement (pos, st) = (** Type of reinitialization data *) type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position +type 'a single_extend_statement = + string option * + (* Level *) + Gramlib.Gramext.g_assoc option * + (* Associativity *) + 'a production_rule list + (* Symbol list with the interpretation function *) + +type 'a extend_statement = + Gramlib.Gramext.position option * + 'a single_extend_statement list + type extend_rule = | ExtendRule : 'a G.Entry.e * gram_reinit option * 'a extend_statement -> extend_rule @@ -462,11 +458,10 @@ module Module = let module_expr = Entry.create "module_expr" let module_type = Entry.create "module_type" end + let epsilon_value (type s tr a) f (e : (s, tr, a) symbol) = - let r = - match symbol_of_prod_entry_key e with - | CastedSNo s -> G.production (G.r_next G.r_stop s, (fun x _ -> f x)) - | CastedSMay s -> G.production (G.r_next G.r_stop s, (fun x _ -> f x)) in + let s = symbol_of_prod_entry_key e in + let r = G.production (G.r_next G.r_stop s, (fun x _ -> f x)) in let ext = [None, None, [r]] in let entry = Gram.entry_create "epsilon" in let warning msg = Feedback.msg_warning Pp.(str msg) in diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 7efeab6ba0..10f78a5a72 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -212,8 +212,19 @@ val epsilon_value : ('a -> 'self) -> ('self, _, 'a) Extend.symbol -> 'self optio type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position (** Type of reinitialization data *) -val grammar_extend : 'a Entry.t -> gram_reinit option -> - 'a Extend.extend_statement -> unit +type 'a single_extend_statement = + string option * + (* Level *) + Gramlib.Gramext.g_assoc option * + (* Associativity *) + 'a production_rule list + (* Symbol list with the interpretation function *) + +type 'a extend_statement = + Gramlib.Gramext.position option * + 'a single_extend_statement list + +val grammar_extend : 'a Entry.t -> gram_reinit option -> 'a extend_statement -> unit (** Extend the grammar of Coq, without synchronizing it with the backtracking mechanism. This means that grammar extensions defined this way will survive an undo. *) diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 60717c6eec..92b7f2accf 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -164,7 +164,7 @@ let prepare_body { Vernacexpr.binders } rt = let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') -let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook = +let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook = (* First we get the type of the old graph principle *) let mutr_nparams = (Tactics.compute_elim_sig !evd (EConstr.of_constr old_princ_type)).Tactics.nparams in (* let time1 = System.get_time () in *) @@ -199,10 +199,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* end; *) let open Proof_global in - let { name; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in + let { name; entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in match entries with | [entry] -> - name, entry, hook + entry, hook | _ -> CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") @@ -282,7 +282,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) register_with_sort Sorts.InProp; register_with_sort Sorts.InSet in - let id,entry,hook = + let entry, hook = build_functional_principle evd interactive_proof old_princ_type new_sorts funs i proof_tac hook in @@ -1170,7 +1170,7 @@ let get_funs_constant mp = in l_const -let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Proof_global.proof_entry list = +let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_effects Declare.proof_entry list = let exception Found_type of int in let env = Global.env () in let funs = List.map fst fas in @@ -1219,9 +1219,21 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef s::l_schemes -> s,l_schemes | _ -> CErrors.anomaly (Pp.str "") in - let _,const,_ = + let opaque = + let finfos = + match find_Function_infos (fst first_fun) with + | None -> raise Not_found + | Some finfos -> finfos + in + let open Proof_global in + match finfos.equation_lemma with + | None -> Transparent (* non recursive definition *) + | Some equation -> + if Declareops.is_opaque (Global.lookup_constant equation) then Opaque else Transparent + in + let entry, _hook = try - build_functional_principle evd false + build_functional_principle ~opaque evd false first_type (Array.of_list sorts) this_block_funs @@ -1233,30 +1245,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef in incr i; - let opacity = - let finfos = - match find_Function_infos (fst first_fun) with - | None -> raise Not_found - | Some finfos -> finfos - in - match finfos.equation_lemma with - | None -> false (* non recursive definition *) - | Some equation -> - Declareops.is_opaque (Global.lookup_constant equation) - in - let const = {const with Proof_global.proof_entry_opaque = opacity } in (* The others are just deduced *) if List.is_empty other_princ_types - then - [const] + then [entry] else let other_fun_princ_types = let funs = Array.map Constr.mkConstU this_block_funs in let sorts = Array.of_list sorts in List.map (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types in - let open Proof_global in - let first_princ_body,first_princ_type = const.proof_entry_body, const.proof_entry_type in + let first_princ_body,first_princ_type = Declare.(entry.proof_entry_body, entry.proof_entry_type) in let ctxt,fix = Term.decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = Constr.destFix fix in let other_result = @@ -1283,7 +1281,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef (* If we reach this point, the two principle are not mutually recursive We fall back to the previous method *) - let _,const,_ = + let entry, _hook = build_functional_principle evd false @@ -1294,20 +1292,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef (Functional_principles_proofs.prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs))) (fun _ _ -> ()) in - const + entry with Found_type i -> let princ_body = Termops.it_mkLambda_or_LetIn (Constr.mkFix((idxs,i),decl)) ctxt in - {const with - proof_entry_body = - (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects)); - proof_entry_type = Some scheme_type - } + Declare.definition_entry ~types:scheme_type princ_body ) other_fun_princ_types in - const::other_result + entry::other_result (* [derive_correctness funs graphs] create correctness and completeness lemmas for each function in [funs] w.r.t. [graphs] @@ -1358,7 +1352,8 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) = Array.of_list (List.map (fun entry -> - (EConstr.of_constr (fst (fst(Future.force entry.Proof_global.proof_entry_body))), EConstr.of_constr (Option.get entry.Proof_global.proof_entry_type )) + (EConstr.of_constr (fst (fst (Future.force entry.Declare.proof_entry_body))), + EConstr.of_constr (Option.get entry.Declare.proof_entry_type )) ) (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs)) ) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index ddd6ecfb5c..7c17ecdba0 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1252,7 +1252,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function | GSort _ -> params | GHole _ -> params | GIf _ | GRec _ | GCast _ -> - raise (UserError(Some "compute_cst_params", str "Not handled case")) + CErrors.user_err ~hdr:"compute_cst_params" (str "Not handled case") ) gt and compute_cst_params_from_app acc (params,rtl) = let is_gid id c = match DAst.get c with GVar id' -> Id.equal id id' | _ -> false in diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index fbf63c69dd..8abccabae6 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -1,4 +1,13 @@ -open Pp +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open Constr open Glob_term open CErrors @@ -433,7 +442,8 @@ let replace_var_by_term x_id term = replace_var_by_pattern lhs, replace_var_by_pattern rhs ) - | GRec _ -> raise (UserError(None,str "Not handled GRec")) + | GRec _ -> + CErrors.user_err (Pp.str "Not handled GRec") | GSort _ | GHole _ as rt -> rt | GInt _ as rt -> rt diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 24b3690138..70211a1860 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open Names open Glob_term diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 2937ae5d14..a205c0744a 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -95,7 +95,8 @@ let functional_induction with_clean c princl pat = (* We need to refresh gl due to the updated evar_map in princ *) Proofview.Goal.enter_one (fun gl -> Proofview.tclUNIT (princ, Tactypes.NoBindings, pf_unsafe_type_of gl princ, args)) - | _ -> raise (UserError(None,str "functional induction must be used with a function" )) + | _ -> + CErrors.user_err (str "functional induction must be used with a function" ) end | Some ((princ,binding)) -> Proofview.tclUNIT (princ, binding, pf_unsafe_type_of gl princ, args) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 7719705138..6d91c2a348 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -40,7 +40,9 @@ let locate_constant ref = let locate_with_msg msg f x = try f x - with Not_found -> raise (CErrors.UserError(None, msg)) + with + | Not_found -> + CErrors.user_err msg let filter_map filter f = @@ -64,8 +66,7 @@ let chop_rlambda_n = | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b | _ -> - raise (CErrors.UserError(Some "chop_rlambda_n", - str "chop_rlambda_n: Not enough Lambdas")) + CErrors.user_err ~hdr:"chop_rlambda_n" (str "chop_rlambda_n: Not enough Lambdas") in chop_lambda_n [] @@ -76,7 +77,8 @@ let chop_rprod_n = else match DAst.get rt with | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b - | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) + | _ -> + CErrors.user_err ~hdr:"chop_rprod_n" (str "chop_rprod_n: Not enough products") in chop_prod_n [] @@ -115,7 +117,7 @@ open DeclareDef let definition_message = Declare.definition_message let save name const ?hook uctx scope kind = - let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in + let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in let r = match scope with | Discharge -> let c = SectionLocalDef const in diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 16beaaa3c7..34fb10bb67 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -44,7 +44,7 @@ val make_eq : unit -> EConstr.constr val save : Id.t - -> Evd.side_effects Proof_global.proof_entry + -> Evd.side_effects Declare.proof_entry -> ?hook:DeclareDef.Hook.t -> UState.t -> DeclareDef.locality diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 0ce726db25..756fef0511 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -6,9 +6,7 @@ Proof Logic Goal_select Proof_bullet -Proof_global Refiner Tacmach -Pfedit Clenv Clenvtac diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index fab6767beb..baa7b3570c 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -11,7 +11,6 @@ open Util let check_vio (ts,f_in) = - Dumpglob.noglob (); let _, _, _, tasks, _ = Library.load_library_todo f_in in Stm.set_compilation_hints f_in; List.fold_left (fun acc ids -> Stm.check_task f_in tasks ids && acc) true ts @@ -142,5 +141,3 @@ let schedule_vio_compilation j fs = List.iter (fun (f,_) -> Unix.utimes (Filename.chop_extension f^".vo") t t) all_jobs; end; exit !rc - - diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 09d7e0278a..edeb27ab88 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -69,7 +69,7 @@ let rec shrink ctx sign c t accu = | _ -> assert false let shrink_entry sign const = - let open Proof_global in + let open Declare in let typ = match const.proof_entry_type with | None -> assert false | Some t -> t @@ -151,7 +151,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = in let const, args = shrink_entry sign const in let args = List.map EConstr.of_constr args in - let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in + let cd = Declare.DefinitionEntry { const with Declare.proof_entry_opaque = opaque } in let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in let cst () = (* do not compute the implicit arguments, it may be costly *) @@ -160,20 +160,20 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = Declare.declare_private_constant ~local:Declare.ImportNeedQualified ~name ~kind cd in let cst, eff = Impargs.with_implicit_protection cst () in - let inst = match const.Proof_global.proof_entry_universes with + let inst = match const.Declare.proof_entry_universes with | Entries.Monomorphic_entry _ -> EInstance.empty | Entries.Polymorphic_entry (_, ctx) -> (* We mimic what the kernel does, that is ensuring that no additional constraints appear in the body of polymorphic constants. Ideally this should be enforced statically. *) - let (_, body_uctx), _ = Future.force const.Proof_global.proof_entry_body in + let (_, body_uctx), _ = Future.force const.Declare.proof_entry_body in let () = assert (Univ.ContextSet.is_empty body_uctx) in EInstance.make (Univ.UContext.instance ctx) in let lem = mkConstU (cst, inst) in let evd = Evd.set_universe_context evd ectx in let effs = Evd.concat_side_effects eff - Proof_global.(snd (Future.force const.proof_entry_body)) in + (snd (Future.force const.Declare.proof_entry_body)) in let solve = Proofview.tclEFFECTS effs <*> tacK lem args diff --git a/tactics/abstract.mli b/tactics/abstract.mli index e278729f89..96ddbea7b2 100644 --- a/tactics/abstract.mli +++ b/tactics/abstract.mli @@ -26,5 +26,5 @@ val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit P save path *) val shrink_entry : ('a, 'b) Context.Named.Declaration.pt list - -> 'c Proof_global.proof_entry - -> 'c Proof_global.proof_entry * Constr.t list + -> 'c Declare.proof_entry + -> 'c Declare.proof_entry * Constr.t list diff --git a/tactics/declare.ml b/tactics/declare.ml index c280760e84..3a02e5451a 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -55,8 +55,20 @@ type constant_obj = { cst_locl : import_status; } +type 'a proof_entry = { + proof_entry_body : 'a Entries.const_entry_body; + (* List of section variables *) + proof_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + proof_entry_feedback : Stateid.t option; + proof_entry_type : Constr.types option; + proof_entry_universes : Entries.universes_entry; + proof_entry_opaque : bool; + proof_entry_inline_code : bool; +} + type 'a constant_entry = - | DefinitionEntry of 'a Proof_global.proof_entry + | DefinitionEntry of 'a proof_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry @@ -174,7 +186,6 @@ let record_aux env s_ty s_bo = let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body = - let open Proof_global in { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); proof_entry_secctx = None; proof_entry_type = types; @@ -184,7 +195,6 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types proof_entry_inline_code = inline} let cast_proof_entry e = - let open Proof_global in let (body, ctx), () = Future.force e.proof_entry_body in let univs = if Univ.ContextSet.is_empty ctx then e.proof_entry_universes @@ -205,7 +215,6 @@ let cast_proof_entry e = } let cast_opaque_proof_entry e = - let open Proof_global in let typ = match e.proof_entry_type with | None -> assert false | Some typ -> typ @@ -224,7 +233,7 @@ let cast_opaque_proof_entry e = let vars = global_vars_set env pf in ids_typ, vars in - let () = if !Flags.record_aux_file then record_aux env hyp_typ hyp_def in + let () = if Aux_file.recording () then record_aux env hyp_typ hyp_def in keep_hyps env (Id.Set.union hyp_typ hyp_def) | Some hyps -> hyps in @@ -249,7 +258,6 @@ let is_unsafe_typing_flags () = not (flags.check_universes && flags.check_guarded && flags.check_positive) let define_constant ~side_effect ~name cd = - let open Proof_global in (* Logically define the constant and its subproofs, no libobject tampering *) let in_section = Lib.sections_are_opened () in let export, decl, unsafe = match cd with @@ -299,7 +307,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind (** Declaration of section variables and local definitions *) type variable_declaration = - | SectionLocalDef of Evd.side_effects Proof_global.proof_entry + | SectionLocalDef of Evd.side_effects proof_entry | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } (* This object is only for things which iterate over objects to find @@ -321,7 +329,6 @@ let declare_variable ~name ~kind d = | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) - let open Proof_global in let (body, eff) = Future.force de.proof_entry_body in let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in let eff = get_roles export eff in diff --git a/tactics/declare.mli b/tactics/declare.mli index 4ae9f6c7ae..4cb876cecb 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -19,14 +19,27 @@ open Entries reset works properly --- and will fill some global tables such as [Nametab] and [Impargs]. *) +(** Proof entries *) +type 'a proof_entry = { + proof_entry_body : 'a Entries.const_entry_body; + (* List of section variables *) + proof_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + proof_entry_feedback : Stateid.t option; + proof_entry_type : Constr.types option; + proof_entry_universes : Entries.universes_entry; + proof_entry_opaque : bool; + proof_entry_inline_code : bool; +} + (** Declaration of local constructions (Variable/Hypothesis/Local) *) type variable_declaration = - | SectionLocalDef of Evd.side_effects Proof_global.proof_entry + | SectionLocalDef of Evd.side_effects proof_entry | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } type 'a constant_entry = - | DefinitionEntry of 'a Proof_global.proof_entry + | DefinitionEntry of 'a proof_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry @@ -43,7 +56,7 @@ val declare_variable val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:types -> ?univs:Entries.universes_entry -> - ?eff:Evd.side_effects -> constr -> Evd.side_effects Proof_global.proof_entry + ?eff:Evd.side_effects -> constr -> Evd.side_effects proof_entry type import_status = ImportDefaultBehavior | ImportNeedQualified diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index e2ef05461b..54393dce00 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -124,17 +124,7 @@ let define internal role id c poly univs = let ctx = UState.minimize univs in let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in let univs = UState.univ_entry ~poly ctx in - let entry = { - Proof_global.proof_entry_body = - Future.from_val ((c,Univ.ContextSet.empty), - Evd.empty_side_effects); - proof_entry_secctx = None; - proof_entry_type = None; - proof_entry_universes = univs; - proof_entry_opaque = false; - proof_entry_inline_code = false; - proof_entry_feedback = None; - } in + let entry = Declare.definition_entry ~univs c in let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id (Declare.DefinitionEntry entry) in let () = match internal with | InternalTacticRequest -> () diff --git a/proofs/pfedit.ml b/tactics/pfedit.ml index 99a254652c..5be7b4fa28 100644 --- a/proofs/pfedit.ml +++ b/tactics/pfedit.ml @@ -124,7 +124,7 @@ let build_constant_by_tactic ~name ctx sign ~poly typ tac = let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in match entries with | [entry] -> - let univs = UState.demote_seff_univs entry.Proof_global.proof_entry_universes universes in + let univs = UState.demote_seff_univs entry.Declare.proof_entry_universes universes in entry, status, univs | _ -> CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") @@ -136,7 +136,7 @@ let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = let name = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in - let body, eff = Future.force ce.Proof_global.proof_entry_body in + let body, eff = Future.force ce.Declare.proof_entry_body in let (cb, ctx) = if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) else body diff --git a/proofs/pfedit.mli b/tactics/pfedit.mli index 0626e40047..30514191fa 100644 --- a/proofs/pfedit.mli +++ b/tactics/pfedit.mli @@ -64,7 +64,7 @@ val build_constant_by_tactic -> poly:bool -> EConstr.types -> unit Proofview.tactic - -> Evd.side_effects Proof_global.proof_entry * bool * UState.t + -> Evd.side_effects Declare.proof_entry * bool * UState.t val build_by_tactic : ?side_eff:bool diff --git a/proofs/proof_global.ml b/tactics/proof_global.ml index 851a3d1135..a2929e45cd 100644 --- a/proofs/proof_global.ml +++ b/tactics/proof_global.ml @@ -24,21 +24,9 @@ module NamedDecl = Context.Named.Declaration (*** Proof Global Environment ***) -type 'a proof_entry = { - proof_entry_body : 'a Entries.const_entry_body; - (* List of section variables *) - proof_entry_secctx : Constr.named_context option; - (* State id on which the completion of type checking is reported *) - proof_entry_feedback : Stateid.t option; - proof_entry_type : Constr.types option; - proof_entry_universes : Entries.universes_entry; - proof_entry_opaque : bool; - proof_entry_inline_code : bool; -} - type proof_object = { name : Names.Id.t - ; entries : Evd.side_effects proof_entry list + ; entries : Evd.side_effects Declare.proof_entry list ; poly : bool ; universes: UState.t ; udecl : UState.universe_decl @@ -223,7 +211,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let ctx = UState.restrict universes used_univs in let univs = UState.check_univ_decl ~poly ctx udecl in (univs, typ), ((body, Univ.ContextSet.empty), eff) - in + in fun t p -> Future.split2 (Future.chain p (make_body t)) else fun t p -> @@ -250,6 +238,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now let t = EConstr.Unsafe.to_constr t in let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in + let open Declare in { proof_entry_body = body; proof_entry_secctx = section_vars; diff --git a/proofs/proof_global.mli b/tactics/proof_global.mli index 54d5c2087a..d15e23c2cc 100644 --- a/proofs/proof_global.mli +++ b/tactics/proof_global.mli @@ -27,29 +27,11 @@ val get_initial_euctx : t -> UState.t val compact_the_proof : t -> t -(** When a proof is closed, it is reified into a [proof_object], where - [id] is the name of the proof, [entries] the list of the proof terms - (in a form suitable for definitions). Together with the [terminator] - function which takes a [proof_object] together with a [proof_end] - (i.e. an proof ending command) and registers the appropriate - values. *) -type 'a proof_entry = { - proof_entry_body : 'a Entries.const_entry_body; - (* List of section variables *) - proof_entry_secctx : Constr.named_context option; - (* State id on which the completion of type checking is reported *) - proof_entry_feedback : Stateid.t option; - proof_entry_type : Constr.types option; - proof_entry_universes : Entries.universes_entry; - proof_entry_opaque : bool; - proof_entry_inline_code : bool; -} - (** When a proof is closed, it is reified into a [proof_object] *) type proof_object = { name : Names.Id.t (** name of the proof *) - ; entries : Evd.side_effects proof_entry list + ; entries : Evd.side_effects Declare.proof_entry list (** list of the proof terms (in a form suitable for definitions). *) ; poly : bool (** polymorphic status *) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 2d0806b2e0..b93c4a176f 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -546,7 +546,8 @@ module New = struct Proofview.tclOR (Proofview.tclTIMEOUT n t) begin function (e, info) -> match e with - | Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (CErrors.print e))) + | Logic_monad.Tac_Timeout as e -> + Proofview.tclZERO (Refiner.FailError (0,lazy (CErrors.print e))) | e -> Proofview.tclZERO ~info e end diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 6dd749aa0d..c5c7969a09 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,4 +1,6 @@ Declare +Proof_global +Pfedit Dnet Dn Btermdn diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 0c0a1897a8..296c253363 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -822,4 +822,4 @@ Defined. Lemma eqb_spec (b b' : bool) : reflect (b = b') (eqb b b'). Proof. destruct b, b'; now constructor. -Qed. +Defined. diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index d8a3dbb4bb..fe5361c156 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -108,8 +108,6 @@ let compile opts copts ~echo ~f_in ~f_out = in match copts.compilation_mode with | BuildVo -> - Flags.record_aux_file := true; - let long_f_dot_v, long_f_dot_vo = ensure_exists_with_prefix f_in f_out ".v" ".vo" in @@ -124,8 +122,11 @@ let compile opts copts ~echo ~f_in ~f_out = Aux_file.(start_aux_file ~aux_file:(aux_file_name_for long_f_dot_vo) ~v_file:long_f_dot_v); + + Dumpglob.set_glob_output copts.glob_out; Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); + let wall_clock1 = Unix.gettimeofday () in let check = Stm.AsyncOpts.(stm_options.async_proofs_mode = APoff) in let state = Vernac.load_vernac ~echo ~check ~interactive:false ~state long_f_dot_v in @@ -139,9 +140,6 @@ let compile opts copts ~echo ~f_in ~f_out = Dumpglob.end_dump_glob () | BuildVio -> - Flags.record_aux_file := false; - Dumpglob.noglob (); - let long_f_dot_v, long_f_dot_vio = ensure_exists_with_prefix f_in f_out ".v" ".vio" in @@ -174,9 +172,6 @@ let compile opts copts ~echo ~f_in ~f_out = Stm.reset_task_queue () | Vio2Vo -> - - Flags.record_aux_file := false; - Dumpglob.noglob (); let long_f_dot_vio, long_f_dot_vo = ensure_exists_with_prefix f_in f_out ".vio" ".vo" in let sum, lib, univs, tasks, proofs = diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 67d70416c8..64c1da20b6 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -59,7 +59,6 @@ type coqargs_config = { debug : bool; diffs_set : bool; time : bool; - glob_opt : bool; print_emacs : bool; set_options : (Goptions.option_name * option_command) list; } @@ -125,7 +124,6 @@ let default_config = { debug = false; diffs_set = false; time = false; - glob_opt = false; print_emacs = false; set_options = []; @@ -380,13 +378,6 @@ let parse_args ~help ~init arglist : t * string list = Flags.compat_version := v; add_compat_require oval v - |"-dump-glob" -> - Dumpglob.dump_into_file (next ()); - { oval with config = { oval.config with glob_opt = true }} - - |"-feedback-glob" -> - Dumpglob.feedback_glob (); oval - |"-exclude-dir" -> System.exclude_directory (next ()); oval @@ -524,7 +515,6 @@ let parse_args ~help ~init arglist : t * string list = |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }} |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }} - |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with config = { oval.config with glob_opt = true }} |"-output-context" -> { oval with post = { oval.post with output_context = true }} |"-profile-ltac" -> Flags.profile_ltac := true; oval |"-q" -> { oval with pre = { oval.pre with load_rcfile = false; }} diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index e414888861..26f22386a0 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -35,7 +35,6 @@ type coqargs_config = { debug : bool; diffs_set : bool; time : bool; - glob_opt : bool; print_emacs : bool; set_options : (Goptions.option_name * option_command) list; } diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 5678acb2b1..019577ac85 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -16,8 +16,7 @@ let outputstate opts = let coqc_init _copts ~opts = Flags.quiet := true; System.trust_file_cache := true; - Coqtop.init_color opts.Coqargs.config; - if not opts.Coqargs.config.Coqargs.glob_opt then Dumpglob.dump_to_dotglob () + Coqtop.init_color opts.Coqargs.config let coqc_specific_usage = Usage.{ executable_name = "coqc"; diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml index 5cced2baac..0b5481fe72 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -23,7 +23,8 @@ type t = ; echo : bool - ; outputstate : string option; + ; outputstate : string option + ; glob_out : Dumpglob.glob_output } let default = @@ -40,6 +41,7 @@ let default = ; echo = false ; outputstate = None + ; glob_out = Dumpglob.MultFiles } let depr opt = @@ -187,6 +189,15 @@ let parse arglist : t = | "-outputstate" -> set_outputstate oval (next ()) + (* Glob options *) + |"-no-glob" | "-noglob" -> + { oval with glob_out = Dumpglob.NoGlob } + + |"-dump-glob" -> + let file = next () in + { oval with glob_out = Dumpglob.File file } + + (* Rest *) | s -> extras := s :: !extras; oval diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli index b02eeeb9ee..13bea3bf3e 100644 --- a/toplevel/coqcargs.mli +++ b/toplevel/coqcargs.mli @@ -24,6 +24,7 @@ type t = ; echo : bool ; outputstate : string option + ; glob_out : Dumpglob.glob_output } val default : t diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 78640334e2..07466d641e 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -438,19 +438,15 @@ let rec loop ~state = loop ~state (* Default toplevel loop *) -let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) let drop_args = ref None + let loop ~opts ~state = drop_args := Some opts; let open Coqargs in print_emacs := opts.config.print_emacs; (* We initialize the console only if we run the toploop_run *) let tl_feed = Feedback.add_feeder coqloop_feed in - if Dumpglob.dump () then begin - Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; - Dumpglob.noglob () - end; let _ = loop ~state in (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 57de719cb4..9745358ba2 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -85,12 +85,12 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o in if program_mode then let env = Global.env () in - let (c,ctx), sideff = Future.force ce.Proof_global.proof_entry_body in + let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); assert(Univ.ContextSet.is_empty ctx); Obligations.check_evars env evd; let c = EConstr.of_constr c in - let typ = match ce.Proof_global.proof_entry_type with + let typ = match ce.Declare.proof_entry_type with | Some t -> EConstr.of_constr t | None -> Retyping.get_type_of env evd c in diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index db0c102e14..01505d0733 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -41,5 +41,5 @@ val interp_definition -> red_expr option -> constr_expr -> constr_expr option - -> Evd.side_effects Proof_global.proof_entry * + -> Evd.side_effects Declare.proof_entry * Evd.evar_map * UState.universe_decl * Impargs.manual_implicits diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 5e4f2dcd34..1926faaf0e 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -44,7 +44,7 @@ end (* Locality stuff *) let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = - let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in + let fix_exn = Future.fix_exn_of ce.proof_entry_body in let gr = match scope with | Discharge -> let () = diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 606cfade46..54a0c9a7e8 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -45,7 +45,7 @@ val declare_definition -> kind:Decls.definition_object_kind -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) -> UnivNames.universe_binders - -> Evd.side_effects Proof_global.proof_entry + -> Evd.side_effects Declare.proof_entry -> Impargs.manual_implicits -> GlobRef.t @@ -66,7 +66,7 @@ val prepare_definition : allow_evars:bool -> ?opaque:bool -> ?inline:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> types:EConstr.t option -> body:EConstr.t -> - Evd.evar_map * Evd.side_effects Proof_global.proof_entry + Evd.evar_map * Evd.side_effects Declare.proof_entry val prepare_parameter : allow_evars:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types -> diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index c5cbb095ca..e3cffa8523 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -149,18 +149,8 @@ let declare_obligation prg obl body ty uctx = if get_shrink_obligations () && not poly then shrink_body body ty else ([], body, ty, [||]) in - let body = - ((body, Univ.ContextSet.empty), Evd.empty_side_effects) - in - let ce = - Proof_global.{ proof_entry_body = Future.from_val ~fix_exn:(fun x -> x) body - ; proof_entry_secctx = None - ; proof_entry_type = ty - ; proof_entry_universes = uctx - ; proof_entry_opaque = opaque - ; proof_entry_inline_code = false - ; proof_entry_feedback = None } - in + let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in + (* ppedrot: seems legit to have obligations as local *) let constant = Declare.declare_constant ~name:obl.obl_name @@ -495,12 +485,11 @@ type obligation_qed_info = } let obligation_terminator entries uctx { name; num; auto } = - let open Proof_global in match entries with | [entry] -> let env = Global.env () in - let ty = entry.proof_entry_type in - let body, eff = Future.force entry.proof_entry_body in + let ty = entry.Declare.proof_entry_type in + let body, eff = Future.force entry.Declare.proof_entry_body in let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in let sigma = Evd.from_ctx uctx in let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in @@ -514,7 +503,7 @@ let obligation_terminator entries uctx { name; num; auto } = let obls, rem = prg.prg_obligations in let obl = obls.(num) in let status = - match obl.obl_status, entry.proof_entry_opaque with + match obl.obl_status, entry.Declare.proof_entry_opaque with | (_, Evar_kinds.Expand), true -> err_not_transp () | (true, _), true -> err_not_transp () | (false, _), true -> Evar_kinds.Define true diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index 2a8fa734b3..7d8a112cc6 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -76,7 +76,7 @@ type obligation_qed_info = } val obligation_terminator - : Evd.side_effects Proof_global.proof_entry list + : Evd.side_effects Declare.proof_entry list -> UState.t -> obligation_qed_info -> unit (** [obligation_terminator] part 2 of saving an obligation *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index cf87646905..a6c577a878 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -98,20 +98,11 @@ let () = (* Util *) -let define ~poly name sigma c t = +let define ~poly name sigma c types = let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in let univs = Evd.univ_entry ~poly sigma in - let open Proof_global in - let kn = f ~name - (DefinitionEntry - { proof_entry_body = c; - proof_entry_secctx = None; - proof_entry_type = t; - proof_entry_universes = univs; - proof_entry_opaque = false; - proof_entry_inline_code = false; - proof_entry_feedback = None; - }) in + let entry = Declare.definition_entry ~univs ?types c in + let kn = f ~name (DefinitionEntry entry) in definition_message name; kn @@ -412,8 +403,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort = let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in let decltype = EConstr.to_constr sigma decltype in - let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in - let cst = define ~poly fi sigma proof_output (Some decltype) in + let cst = define ~poly fi sigma decl (Some decltype) in GlobRef.ConstRef cst :: lrecref in let _ = List.fold_right2 declare listdecl lrecnames [] in @@ -534,7 +524,6 @@ let do_combined_scheme name schemes = schemes in let sigma,body,typ = build_combined_scheme (Global.env ()) csts in - let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Evd.empty_side_effects) in (* It is possible for the constants to have different universe polymorphism from each other, however that is only when the user manually defined at least one of them (as Scheme would pick the @@ -542,7 +531,7 @@ let do_combined_scheme name schemes = some other polymorphism they can also manually define the combined scheme. *) let poly = Global.is_polymorphic (GlobRef.ConstRef (List.hd csts)) in - ignore (define ~poly name.v sigma proof_output (Some typ)); + ignore (define ~poly name.v sigma body (Some typ)); fixpoint_message None [name.v] (**********************************************************************) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 7809425a10..42d1a1f3fc 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -383,10 +383,9 @@ let adjust_guardness_conditions const = function | possible_indexes -> (* Try all combinations... not optimal *) let env = Global.env() in - let open Proof_global in { const with - proof_entry_body = - Future.chain const.proof_entry_body + Declare.proof_entry_body = + Future.chain const.Declare.proof_entry_body (fun ((body, ctx), eff) -> match Constr.kind body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> @@ -404,10 +403,11 @@ let finish_proved env sigma idopt po info = let name = match idopt with | None -> name | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in - let fix_exn = Future.fix_exn_of const.proof_entry_body in + let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in let () = try let const = adjust_guardness_conditions const compute_guard in - let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in + let should_suggest = const.Declare.proof_entry_opaque && + Option.is_empty const.Declare.proof_entry_secctx in let open DeclareDef in let r = match scope with | Discharge -> @@ -451,7 +451,7 @@ let finish_derived ~f ~name ~idopt ~entries = in (* The opacity of [f_def] is adjusted to be [false], as it must. Then [f] is declared in the global environment. *) - let f_def = { f_def with Proof_global.proof_entry_opaque = false } in + let f_def = { f_def with Declare.proof_entry_opaque = false } in let f_kind = Decls.(IsDefinition Definition) in let f_def = Declare.DefinitionEntry f_def in let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in @@ -463,17 +463,17 @@ let finish_derived ~f ~name ~idopt ~entries = let substf c = Vars.replace_vars [f,f_kn_term] c in (* Extracts the type of the proof of [suchthat]. *) let lemma_pretype = - match Proof_global.(lemma_def.proof_entry_type) with + match lemma_def.Declare.proof_entry_type with | Some t -> t | None -> assert false (* Proof_global always sets type here. *) in (* The references of [f] are subsituted appropriately. *) let lemma_type = substf lemma_pretype in (* The same is done in the body of the proof. *) - let lemma_body = Future.chain Proof_global.(lemma_def.proof_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in - let lemma_def = let open Proof_global in + let lemma_body = Future.chain lemma_def.Declare.proof_entry_body (fun ((b,ctx),fx) -> (substf b, ctx), fx) in + let lemma_def = { lemma_def with - proof_entry_body = lemma_body; + Declare.proof_entry_body = lemma_body; proof_entry_type = Some lemma_type } in let lemma_def = Declare.DefinitionEntry lemma_def in @@ -530,7 +530,7 @@ let save_lemma_admitted_delayed ~proof ~info = let { Info.hook; scope; impargs; other_thms } = info in if List.length entries <> 1 then user_err Pp.(str "Admitted does not support multiple statements"); - let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in + let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in let poly = match proof_entry_universes with | Entries.Monomorphic_entry _ -> false | Entries.Polymorphic_entry (_, _) -> true in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 37fe0df0ee..5d153fa8be 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -423,11 +423,11 @@ let solve_by_tac ?loc name evi t poly ctx = Pfedit.build_constant_by_tactic ~name ~poly ctx evi.evar_hyps evi.evar_concl t in let env = Global.env () in - let (body, eff) = Future.force entry.Proof_global.proof_entry_body in + let (body, eff) = Future.force entry.Declare.proof_entry_body in let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); - Some (fst body, entry.Proof_global.proof_entry_type, Evd.evar_universe_context ctx') + Some (fst body, entry.Declare.proof_entry_type, Evd.evar_universe_context ctx') with | Refiner.FailError (_, s) as exn -> let _ = CErrors.push exn in diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 094e2c1184..cfb3248c7b 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -130,7 +130,7 @@ let suggest_common env ppid used ids_typ skip = str "should start with one of the following commands:"++spc()++ v 0 ( prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs)); - if !Flags.record_aux_file + if Aux_file.recording () then let s = string_of_ppcmds (prlist_with_sep (fun _ -> str";") (fun x->x) !valid_exprs) in record_proof_using s diff --git a/vernac/record.ml b/vernac/record.ml index 86745212e7..11237f3873 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -340,16 +340,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in try - let open Proof_global in - let entry = { - proof_entry_body = - Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects); - proof_entry_secctx = None; - proof_entry_type = Some projtyp; - proof_entry_universes = ctx; - proof_entry_opaque = false; - proof_entry_inline_code = false; - proof_entry_feedback = None } in + let entry = Declare.definition_entry ~univs:ctx ~types:projtyp proj in let kind = Decls.IsDefinition kind in let kn = declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) in let constr_fip = |