aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-05-13Create new file on sorts.Théo Zimmermann
2020-05-13Extract Sorts out of CIC.Théo Zimmermann
2020-05-13Merge PR #12293: Fix timestamp of coqchk manpageThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-13Added change log.Hugo Herbelin
2020-05-13Ssrmatching: Hack to circumvent a hack.Hugo Herbelin
2020-05-13Make explicit that UGraph lower bounds are only of two kinds.Pierre-Marie Pédrot
This makes the invariants in the code clearer, and also highlight this is only required to implement template polymorphic inductive types.
2020-05-13do not re-export ListNotations from Program: kill overlaysAntonio Nikishaev
2020-05-13Merge PR #12229: Hopefully consensual cleaning of keywordsThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: jfehrle Ack-by: ppedrot
2020-05-13Merge PR #11828: [obligations] Deprecated flag cleanupGaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: Zimmi48
2020-05-13Centralize the OCaml version-checking function.Pierre-Marie Pédrot
We tweak the message a bit.
2020-05-13Store the OCaml version used for Coq in vo files.Pierre-Marie Pédrot
2020-05-13Test interleaving of command-line options.Théo Zimmermann
2020-05-13Document the changes regarding the order of command-line options.Théo Zimmermann
2020-05-13Clarify the assignee's role in removing the overlay informationAnton Trunov
2020-05-13Fixes #12233 (wrong printing env in presence of match branches eta-expansion).Hugo Herbelin
At the same time, we propagate the correct binder relevance in detyping. Note that this would be fixed by enforcing the context of branches in the syntax of "Case".
2020-05-13Clarify the documentation for merging PRs with overlaysAnton Trunov
2020-05-12Merge PR #12309: Remove documentation of -compile, which was removed in #8690.Clément Pit-Claudel
2020-05-13Merge PR #12307: Cleaning up the legacy proof engineEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-12Merge PR #11503: Allow to rebind the old value of a mutable Ltac2 entry.Jason Gross
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: kyoDralliam
2020-05-12Merge PR #12223: Locating error again in atomic tactics (fixes #12152)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-05-12Remove documentation of -compile, which was removed in #8690.Théo Zimmermann
2020-05-12Merge PR #12162: Fixing #12161: rename Bool.leb into Bool.leAnton Trunov
Ack-by: Zimmi48 Reviewed-by: anton-trunov
2020-05-12Merge PR #12146: Fixes #10812: tactic subst failure with section variables ↵Pierre-Marie Pédrot
indirectly dependent in goal Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-12Merge PR #12190: [stdlib] [Permutation] Declare more instances as GlobalAnton Trunov
Reviewed-by: JasonGross Reviewed-by: anton-trunov
2020-05-12Remove a unused legacy tactic from Clenv.Pierre-Marie Pédrot
2020-05-12Write the outermost part of the legacy refiner directly in the monad.Pierre-Marie Pédrot
2020-05-12Clean up the legacy refiner implementation.Pierre-Marie Pédrot
We avoid using global-access primitives and instead rely on purely functional passing of the relevant data. Namely, we replace the goal argument with its environment, and we pass the additional check parameter.
2020-05-12Interleave commandline require/set/unset commandsLasse Blaauwbroek
2020-05-12Remove legacy Refiner error constructors.Pierre-Marie Pédrot
They were not used anywhere anymore.
2020-05-12Remove useless try-with clauses in newring.Pierre-Marie Pédrot
This is already protected by then enter block.
2020-05-12Wrap the legacy refiner type into the Logic API.Pierre-Marie Pédrot
2020-05-12Do not use Unsafe.to_constr for old refiner conclusion.Pierre-Marie Pédrot
This was useless, since we did not observe the difference on evars.
2020-05-12documenting with examples the dynamic behaviour of Ltac2 SetKenji Maillard
2020-05-12Remove useless try-with blocks in congruence.Pierre-Marie Pédrot
The inner body was not raising any exception since it was in the monad, and even if it did so, the enter block would have caught it.
2020-05-12Merge PR #12303: [changelog] Fuse changelogs for #11249 and #12237Théo Zimmermann
Reviewed-by: Zimmi48
2020-05-12fuse changelogs for #11249 and #12237Olivier Laurent
2020-05-11More tests of rebinding Ltac2 definitionsKenji Maillard
2020-05-11Merge PR #12254: In non-strict mode, accept any variable as a tactic reference.Hugo Herbelin
Reviewed-by: herbelin
2020-05-11Merge PR #10609: Register (for Coqlib.ref_lib) several base datatypes of stdlibHugo Herbelin
Reviewed-by: JasonGross
2020-05-11Checking validity of coqdoc file name.Hugo Herbelin
This fixes #12265 (javascript injection vulnerability in file name).
2020-05-11Merge PR #12273: Deprecate Refiner APIEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-11Correcting ltac2's documentation on values turning test into proper check.Kenji Maillard
2020-05-11Generalize the Ltac2 value criterion to pure let-bindings.Pierre-Marie Pédrot
2020-05-11Allow to rebind the old value of a mutable Ltac2 entry.Pierre-Marie Pédrot
2020-05-11Merge PR #12129: Add a `with_strategy` tacticPierre-Marie Pédrot
Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: herbelin Ack-by: ppedrot
2020-05-10Remove (outdated) timestamps from man pagesKartik Singhal
2020-05-10Add overlays.Pierre-Marie Pédrot
2020-05-10Further cleanup: remove the local_reduction_function type.Pierre-Marie Pédrot
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
This is extracted from #9710, where we need the environment anyway to compute iota rules on inductive types with let-bindings. The commit is self-contained, so I think it could go directly in to save me a few rebases. Furthermore, this is also related to #11707. Assuming we split cbn from the other reduction machine, this allows to merge the "local" machine with the general one, since after this PR they will have the same type. One less reduction machine should make people happy.
2020-05-10Merge PR #12235: Ensure eintros allows creating evarsKenji Maillard
Reviewed-by: kyoDralliam
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-30 01:57:42 +0000