aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-30Merge PR #10949: [declare] Provide helper for private constant inlining.Pierre-Marie Pédrot
Reviewed-by: SkySkimmer Reviewed-by: ppedrot
2019-10-30Merge PR #10681: [declare] Make `proof_entry` a private type.Pierre-Marie Pédrot
2019-10-30Move start_proof_com from lemmas to vernacentriesGaëtan Gilbert
This lets us remove the closure passing for the program inference_hook
2019-10-30add test for #4502 (fixed by unknown commit)Gaëtan Gilbert
Close #4502
2019-10-30Merge PR #10494: Show diffs in "Show Proof."Enrico Tassi
Reviewed-by: Zimmi48 Reviewed-by: gares Ack-by: herbelin
2019-10-30Numbers.Cyclic: use “lia” rather than “omega”Vincent Laporte
2019-10-29Merge PR #10966: `assert_succeeds`&`assert_fails`: multisuccess fixGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2019-10-29Show diffs in "Show Proof."Jim Fehrle
Add experimental "Show Proof" command to the toplevel that shadows the current command in the parser (in coqtop and PG only). Apply existing code to highlight diffs in the output
2019-10-29Use a less kludgy way of solving #9114Jason Gross
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
These tactics now work correctly with multisuccess tactics by wrapping the tactic argument in `once`. Fixes #10965
2019-10-29[abstract] Remove un-unused reference to `evar_map`Emilio Jesus Gallego Arias
We use an `evar_map ref` even tho the modification the `evar_map` is ignored. I'm not sure if this is a bug or not, so I am making thus preserving the behavior but making the what is going with the `evar_map` more explicit.
2019-10-29[declare] Use helper function for `fix_exn` instead of relying on internals.Emilio Jesus Gallego Arias
2019-10-29[declare] Make `proof_entry` a private type.Emilio Jesus Gallego Arias
Proof entries are low-level objects and should not be manipulated by users directly, in particular as we want to unify all the code around declaration of constants. This patch doesn't bring by itself a lot of improvement, other than setting the base where to extend the interface, however it already points out some points of interest, and in particular the manipulation of opacity done by `Derive` which can be quite problematic, and of course the handling of delayed proofs. So while this is a first step, IMHO it doesn't harm a lot having it in place, but a lot more work will be needed, in particular regarding the handling of delayed proofs. To make `proof_entry` a fully abstract type, the remaining work is focused on `abstract` and obligations, both of which do quite a few hackery that will have to be migrated to the `Declare` API.
2019-10-29Merge PR #10892: [engine] Remove UnivGen.global_of_constrPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-10-29Document the ability to bind notation arguments in Ltac2.Pierre-Marie Pédrot
2019-10-29Fix #10615: Notation substitution for Ltac2 terms.Pierre-Marie Pédrot
We implement a new type of "preterms" that represent untyped ASTs, corresponding to glob_expr in the ML implementations. Ltac2 quotations inside notations are provided with such preterms, and have to pretype them in order to do anything of relevance with them.
2019-10-29Merge PR #10942: Describe XML tags used for highlighting diff textThéo Zimmermann
Reviewed-by: Zimmi48
2019-10-29Merge PR #10947: Rename `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in ↵Enrico Tassi
`coq_makefile` Ack-by: SkySkimmer Reviewed-by: gares
2019-10-28Add support for Sorts in numeral notationsJason Gross
2019-10-28Merge PR #10963: Possible simplification of parsing rules.Clément Pit-Claudel
Reviewed-by: ppedrot
2019-10-28Rename `VDFILE` from `.coqdeps.d` to `.<CoqMakefile>.d` in the ↵Kazuhiko Sakaguchi
`coq_makefile` utility The `coq_makefile` utility and `Makefile`s generated by it generate and include some files: `<CoqMakefile>.conf`, `<CoqMakefile>.local`, and the dependency file `.coqdep.d`, where `<CoqMakefile>` is the name of the output file given by the `-o` option. Out of these, only the name of the dependency file `.coqdep.d` is fixed to a constant. This seems to be a potential pitfall when we place multiple `Makefile`s generated by `coq_makefile` in the same directory. This patch renames `.coqdeps.d` to `.<CoqMakefile>.d`.
2019-10-28[declare] Provide helper for private constant inlining.Emilio Jesus Gallego Arias
We factor some duplicate code, this is a step towards making the `proof_entry` type abstract.
2019-10-28Fix typos.Théo Zimmermann
Co-Authored-By: Clément Pit-Claudel <cpitclaudel@users.noreply.github.com>
2019-10-28Merge PR #10944: [meta] Add zify plugin to META file.Vincent Laporte
Reviewed-by: vbgl
2019-10-28[stdlib]Reals: use “lia” rather than “omega”Vincent Laporte
2019-10-28Merge PR #10950: [declare] Split universe and inductive declaration code to ↵Gaëtan Gilbert
vernac/ Ack-by: Janno Reviewed-by: SkySkimmer
2019-10-28Merge PR #10952: [library] [nit] Remove unnecessary type alias.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: ppedrot
2019-10-28Fix #10903: type-in-type allows fixpoints on sprop inductivesGaëtan Gilbert
I still don't know why it produces a Not_found instead of a regular error in coqtop but let's forget about it.
2019-10-28Add changelog for #10963.Théo Zimmermann
2019-10-28Merge PR #10976: Fix link to `coq-notes.md`Théo Zimmermann
Reviewed-by: Zimmi48
2019-10-27Remove the incorrect extra space in Makefile.vofilesscinart
Which results in extra space in filenames when compiling.
2019-10-27Merge PR #10827: Replace classical reals quotient axioms by functional ↵Hugo Herbelin
extensionality Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin Ack-by: maximedenes
2019-10-27Fix link to `coq-notes.md`Michael D. Adams
2019-10-26Merge PR #10516: [funind] Remove duplicate save function.Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: gares
2019-10-26Remove dead code in save_remaining_recthmsGaëtan Gilbert
2019-10-25Merge PR #10962: Add missing instances for `implb` and `xorb` in ZifyBool.vFrédéric Besson
Reviewed-by: fajb
2019-10-25Add 2 missing instances in ZifyBool.vKazuhiko Sakaguchi
2019-10-25Possible simplification of parsing rules.Théo Zimmermann
Noticed by Jim while working on automatic grammar documentation.
2019-10-25[funind] Remove duplicate save function.Emilio Jesus Gallego Arias
AFAICT the reasoning for introducing this function doesn't hold anymore. This is needed for future refactorings that should make some types private.
2019-10-25[declare] Generalize kind type on declareDefEmilio Jesus Gallego Arias
This is useful to remove some duplicate bits in other declare files.
2019-10-25[funind] Removed dead code.Emilio Jesus Gallego Arias
2019-10-25[vernac] [inductive] Remove unused internal export.Emilio Jesus Gallego Arias
2019-10-25[inductive] [declare] Move full inductive declaration to declareIndEmilio Jesus Gallego Arias
Patch suggested by Gaëtan Gilbert
2019-10-24Merge PR #10943: [meta] Add plugin stanza to META so Fl_dynload works for ↵Vincent Laporte
Coq plugins Reviewed-by: vbgl
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ↵Vincent Semeria
homotopy propositions and homotopy sets. Rename local variable R in test Nsatz, to avoid a name collision with the type of real numbers.
2019-10-24[declare] Split inductive declaration code to vernac/Emilio Jesus Gallego Arias
The code is self-contained and only used by commands; this also highlights the several `Libobject.obj` registered for each declaration.
2019-10-24[declare] Split universe declaration code to vernac/Emilio Jesus Gallego Arias
The code is self-contained and only used by commands; this also highlights the several `Libobject.obj` registered for each declaration.
2019-10-24[library] [nit] Remove unnecessary type alias.Emilio Jesus Gallego Arias
2019-10-24Describe XML tags used for highlighting diff textJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 18:29:40 +0000