aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-15Merge PR #10854: Fix alphabetical ordering in contributors to 8.10.0.Clément Pit-Claudel
Ack-by: cpitclaudel Reviewed-by: jfehrle
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-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-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.
2019-10-06Merge PR #10834: Fix #10831: minor issues in documentation of Function.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-10-06Merge PR #10833: 8.10.0 release notes.Vincent Laporte
Reviewed-by: vbgl
2019-10-06Fix #10831: minor issues in documentation of Function.Théo Zimmermann
2019-10-068.10.0 release notes.Théo Zimmermann
2019-10-05Changelog for SProp onGaëtan Gilbert
2019-10-05Merge PR #10763: Fix syntax of reduction tactics when listing qualid to ↵Vincent Laporte
reduce or not. Reviewed-by: jfehrle
2019-10-05Remove "is_polymorphic_univ" checks in upper layers.Gaëtan Gilbert
There were 2: - when declaring a constraint to avoid monomorphic constraint referring to polymorphic univs, this check is redundant with the check in Section.ml - when declaring a universe context to avoid redeclaring universes, this is not necessary after recent commits.
2019-10-05Fix #10669 incorrect substitution in context outside sectionGaëtan Gilbert
2019-10-05Cleanup ComAssumptionGaëtan Gilbert
The general idea is to move tests on scope=Discharge and on Lib.sections_are_opened up in the call stack. This allows better control over the universe manipulation. There are some corner case behaviour change, eg: - [Context (foo:=bla)] outside a section correctly declares an axiom (fix #10668) - (not observable) universes for [Variable A B : Type] in section are declared only once - universes and universe names for [Axiom A B : Type] are declared only once. This changes the qualification of the universe name: before it was the last axiom (so [B.u0]), now it's the first one ([A.u0]). Probably nobody cares about this. - context outside section uses different [kind] I'm not sure why context outside a section behaves differently based on whether we're in a module type, I tried to preserve it but maybe we should uniformize. The universe manipulation for Axiom (in the declare_assumptions function) is a bit awkward, maybe when there are multiple monomorphic axioms instead of trying to attach the universes to the first one we should just declare them separately like with Context. OTOH unlike with context dropping the universe names seems incorrect.
2019-10-05Move do_primitive from comassumption to its own module.Gaëtan Gilbert
Primitives don't have anything to do with assumptions.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 16:45:15 +0000