aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-29Merge PR #10966: `assert_succeeds`&`assert_fails`: multisuccess fixGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
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
2019-10-22Merge PR #10875: [Stdlib] Remove some uses of the “omega” tacticFrédéric Besson
Reviewed-by: fajb
2019-10-22Merge PR #10899: Fixes #10894 regression: uconstr was not anymore typed in ↵Pierre-Marie Pédrot
the Ltac-substituted environment Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-22Merge PR #10886: test-suite/Makefile: work when manually involved for ↵Enrico Tassi
dune-compiled Coq Reviewed-by: gares
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 10:34:25 +0000