aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-10-18Merge PR #10915: Fix link to `xml-protocol.md` in `dev/README.md`Théo Zimmermann
2019-10-18Fix votour after the change of representation of opaques.Pierre-Marie Pédrot
2019-10-18Allow to pass Ltac1 values to Ltac2 quotations.Pierre-Marie Pédrot
2019-10-17Fix link to `xml-protocol.md` in `dev/README.md`Michael D. Adams
2019-10-17Fix Locate printing regressionGuillaume Melquiond
2019-10-16re-expose UState.demote_seff_univsGaëtan Gilbert
2019-10-16Simplify future forcing in Declare.Pierre-Marie Pédrot
2019-10-16Ensure that side-effect declarations reaching the kernel are forced.Pierre-Marie Pédrot
2019-10-16Split the function used to declare side-effects from the standard one.Pierre-Marie Pédrot
2019-10-16Cleaning up the previous code by ensuring statically invariants on opaque pro...Pierre-Marie Pédrot
2019-10-16Make explicit the delayed computation of opaque bodies in Term_typing.Pierre-Marie Pédrot
2019-10-16Merge PR #10885: Remove [in_section] arguments to Safe_typing functionsPierre-Marie Pédrot
2019-10-16[engine] Remove UnivGen.global_of_constrVincent Laporte
2019-10-16Fix a De Bruijn bug in the computation of term relevance in the kernel.Pierre-Marie Pédrot
2019-10-16Define sphinx replacements for \SProp \Type etcGaëtan Gilbert
2019-10-16Merge PR #10896: Assign ownership of the test-suite compat filesThéo Zimmermann
2019-10-15Merge PR #10854: Fix alphabetical ordering in contributors to 8.10.0.Clément Pit-Claudel
2019-10-15Merge PR #10882: Document Gaëtan's new script to prefill a changelog entry.Clément Pit-Claudel
2019-10-14Fix coq#4741: Extract Constant/Inductive with JSONHelge Bahmann
2019-10-14Assign ownership of the test-suite compat filesJason Gross
2019-10-14Merge PR #10883: Doc update with mlg extension - fix #10855Jason Gross
2019-10-14Merge PR #10852: Fix #10842: incorrect handling of unicode input before spacePierre-Marie Pédrot
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
2019-10-14test-suite/Makefile: work when manually involved for dune-compiled CoqGaëtan Gilbert
2019-10-14Remove obj_sec field of Nametab.obj_prefix record.Gaëtan Gilbert
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
2019-10-14Merge PR #10887: fix rev_right_loop docEnrico Tassi
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
2019-10-14Merge PR #10889: Fix #10888: Context import behaviour in modtypePierre-Marie Pédrot
2019-10-14Merge PR #10881: [make] separate generated gramlib ml files from mli files (f...Vincent Laporte
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 demote_seff_...Pierre-Marie Pédrot
2019-10-13Merge PR #10670: ComAssumption cleanupPierre-Marie Pédrot
2019-10-12Merge PR #10818: Merge Direct and Indirect nodes in Opaqueproof.Maxime Dénès
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
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
2019-10-11Merge PR #10828: Simple script to prefill a changelog entryThéo Zimmermann
2019-10-11Merge PR #10804: Fix Print All of section variablesPierre-Marie Pédrot
2019-10-11Merge PR #10850: chmod -x some filesGaëtan Gilbert
2019-10-11Merge PR #10697: [vernac] Split vernacular translation and interpretation.Gaëtan Gilbert
2019-10-11Simple script to prefill a changelog entryGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 06:43:35 +0000