aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-03-31Merge PR #9841: Remove some [let foo = foo] in eqschemesPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-03-31Move content of COMPATIBILITY to Changes chapter.Théo Zimmermann
2019-03-31Move V8 CHANGES to Changes chapter.Théo Zimmermann
2019-03-31Move V7 CHANGES to History chapter.Théo Zimmermann
2019-03-31Change main sections in history chapter.Théo Zimmermann
2019-03-31Split credits chapter in two parts: history, and changelog in inverse ↵Théo Zimmermann
chronological order.
2019-03-31Merge PR #9800: Less conv_tab allocations when pushing relevances, esp ↵Pierre-Marie Pédrot
skip_pattern Reviewed-by: ppedrot
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
(warn if bar is a nonprimitive projection)
2019-03-30Merge PR #8730: Add unicode category LMPierre-Marie Pédrot
Reviewed-by: jashug Ack-by: ppedrot Reviewed-by: vbgl
2019-03-30Merge pull request coq/ltac2#86 from ejgallego/more-dunePierre-Marie Pédrot
[dune] Full Dune support.
2019-03-30[vernac] Small cleanup to remove assert false.Emilio Jesus Gallego Arias
This is a fairly small cleanup on the `vernac_interp` function, which makes code cleaner and for example would allow to have `Load` inside `Load`. [Not that we would ever want that]
2019-03-30[program] Allow evars in type of fixpoints.Emilio Jesus Gallego Arias
This is the right thing to do until we refine the program architecture a bit to use EConstr. Closes #9163 .
2019-03-30Overlay for ElpiVincent Laporte
2019-03-30[Canonical structures] Minor refactoringVincent Laporte
2019-03-30[Canonical structures] Minor cleaningVincent Laporte
2019-03-30[Manual] TypoVincent Laporte
2019-03-30Merge PR #9869: [CI] Force caching when running test-suite in async modeEmilio Jesus Gallego Arias
2019-03-29Merge PR #9858: Fix top_printers after removal of imperative stateEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-29Merge PR #9830: [parser] initialization based on Loc.t rather than Loc.sourceEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Ack-by: gares
2019-03-29[CI] Force caching when running test-suite in async modeMaxime Dénès
I thought the test-suite infrastructure was always passing `-async-proofs-cache force`, but in fact it does it only for interactive tests. This should speed up the tests quite a bit.
2019-03-29Merge PR #9866: typo in ring.rstThéo Zimmermann
Reviewed-by: Zimmi48
2019-03-29Merge PR #9860: [dune] Fix shim quoting and add coqc wrapper.Théo Zimmermann
Reviewed-by: Zimmi48
2019-03-29Merge PR #9859: [dune] Don't regenerate ltac/dune after bootstrapping.Théo Zimmermann
Reviewed-by: Zimmi48
2019-03-29Merge PR #9853: Use only lowercase for unimath in CI scriptsEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-03-29typo in ring.rstthery
2019-03-29[parser] initialization based on Loc.t rather than Loc.sourceEnrico Tassi
In this way one can also set the current offsets in a file, useful if you are parsing a Coq fragment within a file instead of a full file starting from the first line.
2019-03-29[dune] Full Dune support.Emilio Jesus Gallego Arias
This add experimental support for building the full Ltac2 plugin with Dune, see tree at https://github.com/ejgallego/dune/tree/coq
2019-03-29Merge PR #9834: Ignore generated files for CoqIDE bindingsGaëtan Gilbert
Reviewed-by: gares
2019-03-28Merge pull request coq/ltac2#109 from ejgallego/proof+no_global_partialPierre-Marie Pédrot
[coq] Adapt to coq/coq#9129 "removal of imperative proof state"
2019-03-28[dune] Fix shim quoting and add coqc wrapper.Emilio Jesus Gallego Arias
The quoting was incorrect thus scripts didn't properly work.
2019-03-28[dune] Don't regenerate ltac/dune after bootstrapping.Emilio Jesus Gallego Arias
Once we have the good `plugins/ltac/dune` in place for bootstrapping, we should not regenerate it. Thanks to @maximedenes for the report. This fixes `make states` always rebuilding ltac's dependencies.
2019-03-28Fix top_printers after removal of imperative stateGaëtan Gilbert
There's never a proof available in ocamldebug I don't know about Drop.
2019-03-28Use only lowercase for unimath in CI scriptsGaëtan Gilbert
Fix #9845
2019-03-28Merge PR #9129: [proof] Removal of imperative state ; interpretation layers ↵Maxime Dénès
only. Ack-by: SkySkimmer Reviewed-by: aspiwack Ack-by: ejgallego Ack-by: gares Ack-by: herbelin Reviewed-by: mattam82 Ack-by: maximedenes
2019-03-28Merge PR #9743: Relax the ambiguous path condition of coercionEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: gares Ack-by: pi8027
2019-03-28Merge PR #9850: [dune] Don't have `lib` depend on `dynlink`Théo Zimmermann
Reviewed-by: Zimmi48
2019-03-27Merge PR #9828: Fix syntax of Typeclasses eauto := in reference manual.Jim Fehrle
2019-03-28[dune] Don't have `lib` depend on `dynlink`Emilio Jesus Gallego Arias
This is convenient for the bootstrap of `coqdep`
2019-03-27[doc] [abstract] Document a bit some problems with abstract.Emilio Jesus Gallego Arias
2019-03-27[funind] Try to be more precise with universe contexts in recdef hooks.Emilio Jesus Gallego Arias
2019-03-27[proof_global] [ci] Overlays for removal of imperative state.Emilio Jesus Gallego Arias
2019-03-27[geninterp] Track polymorphic status in tactic interpretation.Emilio Jesus Gallego Arias
2019-03-27[vernac] [stm] Tweak `with_fail` and hopefully fix the semantics.Emilio Jesus Gallego Arias
We try to do a bit of cleanup for the `with_fail` function, this still is delicate code.
2019-03-27[vernac] Thread proof state to declare_assumption for warningEmilio Jesus Gallego Arias
Not sure the warning is worth the extra parameter.
2019-03-27[vernacular] Make `Show` fail again when no goals remain.Emilio Jesus Gallego Arias
This is used in the test-suite to check that a proof is closed; I am not sure we'd like to keep this patch tho: the non-failing semantics seems saner for IDEs. [main users are in `test-suite/ide`]
2019-03-27[vernac] Allow path for `save_proof` where no proof state is present.Emilio Jesus Gallego Arias
In that case the terminator and proof object have to be supplied in the ?proof argument, or else we get an anomaly. Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
2019-03-27[plugin tutorial] Adapt to removal of imperative state.Emilio Jesus Gallego Arias
2019-03-27[plugins] [funind] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27[plugins] [extraction] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27[plugins] [derive] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-14 05:19:26 +0000