aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-15Merge PR #10882: Document Gaëtan's new script to prefill a changelog entry.Clément Pit-Claudel
Ack-by: SkySkimmer Reviewed-by: cpitclaudel
2019-10-14Fix coq#4741: Extract Constant/Inductive with JSONHelge Bahmann
Resolve by consulting is_custom/find_custom.
2019-10-14Assign ownership of the test-suite compat filesJason Gross
I want to be notified when these are changed
2019-10-14Merge PR #10883: Doc update with mlg extension - fix #10855Jason Gross
Reviewed-by: JasonGross Reviewed-by: gares Ack-by: ppedrot
2019-10-14Merge PR #10852: Fix #10842: incorrect handling of unicode input before spacePierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-10-14Updating changelogHugo Herbelin
2019-10-14ClassicalFacts.v: Unifying format for bibliographical references.Hugo Herbelin
2019-10-14Weak excluded-middle: adding a reference.Hugo Herbelin
2019-10-14Logic: Add equivalence between weak excluded-middle and classical Morgan's lawHugo Herbelin
2019-10-14Fix #9851: anomaly when unsolved evar in Add RingGaëtan Gilbert
AFAICT there is no reason to use interp_open_constr I used Evd.from_ctx to keep passing evar maps around but maybe we should be passing ustates instead?
2019-10-14test-suite/Makefile: work when manually involved for dune-compiled CoqGaëtan Gilbert
i.e. you can do ~~~ make -f Makefile.dune world make -C test-suite success ~~~ to make just the success tests, then modify Coq sources and retest just the ones you want
2019-10-14Remove obj_sec field of Nametab.obj_prefix record.Gaëtan Gilbert
There are no more users.
2019-10-14Use kernel info from Global for Lib.sections_{depth,are_opened}Gaëtan Gilbert
2019-10-14Remove [in_section] arguments to Safe_typing functionsGaëtan Gilbert
The information is already there. At some point we may want to clean up the Lib API to reduce redundancy wrt kernel functions like [sections_are_opened], but I'm not doing now as it would conflict with https://github.com/coq/coq/pull/10670
2019-10-14Merge PR #10887: fix rev_right_loop docEnrico Tassi
Reviewed-by: gares
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-14Merge PR #10889: Fix #10888: Context import behaviour in modtypePierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-14Merge PR #10881: [make] separate generated gramlib ml files from mli files ↵Vincent Laporte
(fix #10864) Reviewed-by: SkySkimmer
2019-10-13Doc update with mlg extension - fix #10855mcaci
2019-10-13Fix #10888: Context import behaviour in modtypeGaëtan Gilbert
2019-10-13fix rev_right_loop docAntonio Nikishaev
2019-10-13Merge PR #10862: Simplify universe handling wrt side effects: rm ↵Pierre-Marie Pédrot
demote_seff_univs Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-13Merge PR #10670: ComAssumption cleanupPierre-Marie Pédrot
Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
2019-10-12Merge PR #10818: Merge Direct and Indirect nodes in Opaqueproof.Maxime Dénès
Reviewed-by: gares
2019-10-12[make] separate generated gramlib ml files from mli files (fix #10864)Enrico Tassi
2019-10-11Merge PR #10489: Fix output for "Printing Dependent Evars Line"Hugo Herbelin
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: hendriktews Reviewed-by: herbelin Ack-by: mattam82
2019-10-11Document Gaëtan's new script to prefill a changelog entry.Théo Zimmermann
2019-10-11Merge PR #10740: More precise error messages for `Add Ring`Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-11Merge PR #10828: Simple script to prefill a changelog entryThéo Zimmermann
Reviewed-by: Zimmi48
2019-10-11Merge PR #10804: Fix Print All of section variablesPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-11Merge PR #10850: chmod -x some filesGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: ppedrot
2019-10-11Merge PR #10697: [vernac] Split vernacular translation and interpretation.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2019-10-11Simple script to prefill a changelog entryGaëtan Gilbert
2019-10-11Merge PR #10844: Bump version number to 8.11.Théo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-10-10Merge PR #10817: Remove redundancy in section hypotheses of kernel entries.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-10-09Specialize UState.merge for extend:falseGaëtan Gilbert
It's only called with extend:false from inside UState so we don't need to expose it. Not having to look at the whole `merge` function will hopefully help those trying to understand side effects.
2019-10-09Simplify universe handling wrt side effects: rm demote_seff_univsGaëtan Gilbert
We don't need to call `UState.demote_seff_univs` as `emit_side_effects` (`tclEFFECTS`) can do it for us.
2019-10-09A few fixes to the CREDITS file.Théo Zimmermann
Move to the right alphabetical ordering, fix dates, institutions. Also add Jim, but not all the other missing people because I officially renounce to keeping this file up-to-date.
2019-10-09Fix alphabetical ordering in the list of contributors to 8.10.Théo Zimmermann
Also remove Pierre Letouzey from the list because his contribution was the numeral notation feature which ended up being backported to 8.9, after the branching, but before the first beta release.
2019-10-08Merge PR #10840: Release process: release notesThéo Zimmermann
Reviewed-by: Zimmi48
2019-10-08Merge PR #10791: Replace custom timeout logic with new GitLab's per-job ↵Emilio Jesus Gallego Arias
timeout keyword. Reviewed-by: ejgallego
2019-10-08Merge PR #10770: [ci] Add mit-pdos/perennialEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-10-08Merge PR #10780: [CI/Azure/macOS] Update GTK3 to 3.24.11Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-10-08Fix #10842: incorrect handling of unicode input before spacecharguer
2019-10-07chmod -x some filesJason Gross
They probably don't need to be executable
2019-10-07Release process: release notesVincent Laporte
Explain into the release process how to prepare the release notes.
2019-10-07Call to update-compat.py.Pierre-Marie Pédrot
2019-10-07Bump version number to 8.11.Pierre-Marie Pédrot
2019-10-07Merge PR #9933: Add a few missing notes to the release doc.Vincent Laporte
Ack-by: ejgallego Reviewed-by: vbgl
2019-10-07[vernac] Split vernacular translation and interpretation.Emilio Jesus Gallego Arias
This allows UI clients to implement a different state management strategy with regards to proofs, and in particular to override `Vernacinterp.interp`. This is work in progress towards having a true `VtTactic` which shall not perform any state changes non-functionally, and actually removing the series of `assert false` due to meta-vernacs.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 23:51:17 +0000