aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-30[refman] Add a second example of contradiction when positivity checking is ↵Théo Zimmermann
disabled.
2019-10-30[refman] Give an example of contradiction when positivity checking is disabled.Théo Zimmermann
2019-10-30Merge PR #10981: [abstract] Remove un-unused reference to `evar_map`Pierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2019-10-30Merge PR #10303: Raise an anomaly when looking up unknown constant/inductivePierre-Marie Pédrot
Reviewed-by: ppedrot
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-30Merge PR #10494: Show diffs in "Show Proof."Enrico Tassi
Reviewed-by: Zimmi48 Reviewed-by: gares Ack-by: herbelin
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-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-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-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-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-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-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
2019-10-24[meta] Add plugin stanza to META so Fl_dynload works for Coq pluginsEmilio Jesus Gallego Arias
This should be backported to 8.10.
2019-10-24Raise an anomaly when looking up unknown constant/inductiveGaëtan Gilbert
If you have access to a kernel name you also should have the environment in which it is defined, barring hacks. In order to disfavor hacks we make the standard lookups raise anomalies so that people are forced to admit they rely on the internals of the environment. We find that hackers operated on the code for side effects, for finding inductive schemes, for simpl and for Print Assumptions. They attempted to operate on funind but the error handling code they wrote would have raised another Not_found instead of being useful. All these uses are indeed hacky so I am satisfied that we are not forcing new hacks on callers.
2019-10-24Merge PR #10945: Release notes for Coq 8.10.1Théo Zimmermann
Reviewed-by: Zimmi48
2019-10-24Release notes for Coq 8.10.1Vincent Laporte
2019-10-24Merge PR #10938: Better wording for "Show Proof" and fix typosThéo Zimmermann
Reviewed-by: Zimmi48
2019-10-24[meta] Add zify plugin to META file.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:22:00 +0000