aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-03-13[Sphinx] Mention licenseMaxime Dénès
2018-03-13[Sphinx] Remove ad-hoc color for links interfering with TOCMaxime Dénès
2018-03-13[Sphinx] Update some metadataMaxime Dénès
2018-03-13[Sphinx] Read version number from configureMaxime Dénès
2018-03-13[Sphinx] Comment out metadata for unused backendsMaxime Dénès
2018-03-13[Sphinx] Remove information for .chm backendMaxime Dénès
2018-03-13[Sphinx] add bibliographyMaxime Dénès
2018-03-13[Sphinx] Add indexesMaxime Dénès
2018-03-12[Sphinx] Add table of contentsMaxime Dénès
2018-03-12Fix whitespace issue in TacticNotationsVisitor.pyMaxime Dénès
2018-03-12[Sphinx] Add doc preambleMaxime Dénès
2018-03-12[Sphinx] Add a few grammar constructionsMaxime Dénès
2018-03-11[vernac] Move `Quit` and `Drop` to the toplevel layer.Emilio Jesus Gallego Arias
2018-03-11[stm] Never consider `Backtrack` as part of the script.Emilio Jesus Gallego Arias
2018-03-11[META] Update Coq version number.Emilio Jesus Gallego Arias
2018-03-10Merge pull request coq/ltac2#46 from ejgallego/located+libnamesPierre-Marie Pédrot
2018-03-10Merge pull request coq/ltac2#47 from ejgallego/ssr+correct_packingPierre-Marie Pédrot
2018-03-10Merge PR #6869: [ssreflect] Fix module scoping problems due to packing and ml...Maxime Dénès
2018-03-10[ssreflect] Fix module scoping problems due to packing and mli files.Emilio Jesus Gallego Arias
2018-03-10Merge PR #6837: [located] Push inner locations in reference to a CAst.t node.Maxime Dénès
2018-03-10Merge PR #6831: [located] More work towards using CAst.tMaxime Dénès
2018-03-10[test-suite] Add backtracking test for `Load`.Emilio Jesus Gallego Arias
2018-03-10[coq] Adapt to coq/coq#6837.Emilio Jesus Gallego Arias
2018-03-10[coq] Adapt to coq/coq#6831.Emilio Jesus Gallego Arias
2018-03-09[doc] Document removal of deprecated options.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-09Merge PR #6946: Fix expected number of arguments for cumulative constructors.Maxime Dénès
2018-03-09Merge PR #6949: Revert PR #873: New strategy based on open scopes for decidin...Maxime Dénès
2018-03-09Fix expected number of arguments for cumulative constructors.Gaëtan Gilbert
2018-03-09Merge PR #6775: Allow using cumulativity without forcing strict constraints.Maxime Dénès
2018-03-09Revert "Merge PR #873: New strategy based on open scopes for deciding which n...Maxime Dénès
2018-03-09Merge PR #6953: [default.nix] Pin nixpkgs version to include Sphinx dependenciesMaxime Dénès
2018-03-09Merge PR #6806: Adding missing unification constraint noticed by @skyskimmerMaxime Dénès
2018-03-09Merge PR #6769: Split closure cache and remove whd_bothMaxime Dénès
2018-03-09Merge PR #6923: Export optionsMaxime Dénès
2018-03-09[default.nix] Pin nixpkgs version to include Sphinx dependenciesVincent Laporte
2018-03-09[default.nix] minor cleaningVincent Laporte
2018-03-09Overlay for Elpi.Gaëtan Gilbert
2018-03-09Adjust EConstr.cmp_constructors for relaxed constructor cumulativityGaëtan Gilbert
2018-03-09Documentation for Cumulativity Weak Constraints.Gaëtan Gilbert
2018-03-09Delayed weak constraints for cumulative inductive types.Gaëtan Gilbert
2018-03-09Statically enforce that ULub is only between levels.Gaëtan Gilbert
2018-03-09Option for messing with inference of irrelevant constraintsGaëtan Gilbert
2018-03-09Cumulativity: improve treatment of irrelevant universes.Gaëtan Gilbert
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-03-09Merge PR #6480: Allow Prop as source for coercionsMaxime Dénès
2018-03-09Merge PR #6947: coqide: queries from the query window are routed there (fix #...Maxime Dénès
2018-03-09Adding a missing unification in typing.ml.Hugo Herbelin
2018-03-09Merge PR #6818: Sphinx doc infrastructureMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 16:27:57 +0000