aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)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
Code from Paul Steckler (MIT).
2018-03-11[vernac] Move `Quit` and `Drop` to the toplevel layer.Emilio Jesus Gallego Arias
This is a first step towards moving REPL-specific commands out of the core layers. In particular, we remove `Quit` and `Drop` from the core vernacular to specific toplevel-level parsing rules.
2018-03-11[stm] Never consider `Backtrack` as part of the script.Emilio Jesus Gallego Arias
This makes Emacs's `Backtrack` commands to be similar to `EditAt`, thus they will correctly revert the document state. This fixes #6240 and likely some other synchronization bugs. It is still unfortunate that true meta commands are part of the vernacular, we should fix this for 8.9.
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
[coq] Adapt to coq/coq#6837.
2018-03-10Merge pull request coq/ltac2#47 from ejgallego/ssr+correct_packingPierre-Marie Pédrot
[coq] Adapt to correct LTAC module packing coq/coq#6869
2018-03-10Merge PR #6869: [ssreflect] Fix module scoping problems due to packing and ↵Maxime Dénès
mli files.
2018-03-10[ssreflect] Fix module scoping problems due to packing and mli files.Emilio Jesus Gallego Arias
Unfortunately, mli-only files cannot be included in packs, so we have the weird situation that the scope for `Tacexpr` is wrong. So we cannot address the module as `Ltac_plugin.Tacexpr` but it lives in the global namespace instead. This creates problem when using other modular build/packing strategies [such as #6857] This could be indeed considered a bug in the OCaml compiler. In order to remedy this situation we face two choices: - leave the module out of the pack (!) - create an implementation for the module I chose the second solution as it seems to me like the most sensible choice. cc: #6512.
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
Closes #6793.
2018-03-10[coq] Adapt to coq/coq#6837.Emilio Jesus Gallego Arias
Minor.
2018-03-10[coq] Adapt to coq/coq#6831.Emilio Jesus Gallego Arias
This removes uses of `Loc.t` in favor of `CAst.t`.
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
The `reference` type contains some ad-hoc locations in its constructors, but there is no reason not to handle them with the standard attribute container provided by `CAst.t`. An orthogonal topic to this commit is whether the `reference` type should contain a location or not at all. It seems that many places would become a bit clearer by splitting `reference` into non-located `reference` and `lreference`, however some other places become messier so we maintain the current status-quo for now.
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
We continue with the work of #402 and #6745 and update most of the remaining parts of the AST: - module declarations - intro patterns - top-level sentences Now, parsed documents should be full annotated by `CAst` nodes.
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 ↵Maxime Dénès
deciding…
2018-03-09Fix expected number of arguments for cumulative constructors.Gaëtan Gilbert
We expected `nparams + nrealargs + consnrealargs` but the `nrealargs` should not be there. This breaks cumulativity of constructors for any inductive with indices (so records still work, explaining why the test case in #6747 works).
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 ↵Maxime Dénès
notation to use among several of them" This reverts commit 9cac9db6446b31294d2413d920db0eaa6dd5d8a6, reversing changes made to 2f679ec5235257c9fd106c26c15049e04523a307.
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
When comparing 2 irrelevant universes [u] and [v] we add a "weak constraint" [UWeak(u,v)] to the UState. Then at minimization time a weak constraint between unrelated universes where one is flexible causes them to be unified.
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
In Reductionops.infer_conv we did not have enough information to properly try to unify irrelevant universes. This requires changing the Reduction.universe_compare type a bit.
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative inductive would try to generate a constraint [i = j] and use cumulativity only if this resulted in an inconsistency. This is confusingly different from the behaviour with [Type] and means cumulativity can only be used to lift between universes related by strict inequalities. (This isn't a kernel restriction so there might be some workaround to send the kernel the right constraints, but not in a nice way.) See modified test for more details of what is now possible. Technical notes: When universe constraints were inferred by comparing the shape of terms without reduction, cumulativity was not used and so too-strict equality constraints were generated. Then in order to use cumulativity we had to make this comparison fail to fall back to full conversion. When unifiying 2 instances of a cumulative inductive type, if there are any Irrelevant universes we try to unify them if they are flexible.
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
#5684)
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-06-23 01:45:29 +0000