aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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-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-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
2019-10-23Better wording for "Show Proof" and fix typosJim Fehrle
2019-10-23Merge PR #10932: Add a notation for the empty type.Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: amahboubi
2019-10-23Merge PR #10929: documentation fixesThéo Zimmermann
Ack-by: Zimmi48 Reviewed-by: jfehrle
2019-10-23Merge PR #10884: Last stop before CEP 40Maxime Dénès
Reviewed-by: SkySkimmer Reviewed-by: ejgallego Reviewed-by: gares
2019-10-23Merge PR #10897: Fix coq#4741: Extract Constant/Inductive with JSONVincent Laporte
Reviewed-by: vbgl
2019-10-22documentation fixesAntonio Nikishaev
document « Property » more documentation fixes [doc] destructed → destructured [doc] another le_minus→lt_1_r [doc] @jfehrle suggestions [doc] more minor fixes
2019-10-22Merge PR #10880: Allow to pass Ltac1 values to Ltac2 quotations.Jason Gross
Ack-by: SkySkimmer Reviewed-by: Zimmi48
2019-10-22Update doc/changelog/06-ssreflect/10932-void-type-ssr.rst Arthur Azevedo de Amorim
Improve changelog. Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-10-22Update changelog.Arthur Azevedo de Amorim
2019-10-22Add a notation for the empty type.Arthur Azevedo de Amorim
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:17:53 +0000