| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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.t | Emilio 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-09 | Merge PR #6946: Fix expected number of arguments for cumulative constructors. | Maxime Dénès | |
| 2018-03-09 | Merge PR #6949: Revert PR #873: New strategy based on open scopes for ↵ | Maxime Dénès | |
| deciding… | |||
| 2018-03-09 | Fix 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-09 | Merge PR #6775: Allow using cumulativity without forcing strict constraints. | Maxime Dénès | |
| 2018-03-09 | Revert "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-09 | Merge PR #6953: [default.nix] Pin nixpkgs version to include Sphinx dependencies | Maxime Dénès | |
| 2018-03-09 | Merge PR #6806: Adding missing unification constraint noticed by @skyskimmer | Maxime Dénès | |
| 2018-03-09 | Merge PR #6769: Split closure cache and remove whd_both | Maxime Dénès | |
| 2018-03-09 | Merge PR #6923: Export options | Maxime Dénès | |
| 2018-03-09 | [default.nix] Pin nixpkgs version to include Sphinx dependencies | Vincent Laporte | |
| 2018-03-09 | [default.nix] minor cleaning | Vincent Laporte | |
| 2018-03-09 | Overlay for Elpi. | Gaëtan Gilbert | |
| 2018-03-09 | Adjust EConstr.cmp_constructors for relaxed constructor cumulativity | Gaëtan Gilbert | |
| 2018-03-09 | Documentation for Cumulativity Weak Constraints. | Gaëtan Gilbert | |
| 2018-03-09 | Delayed 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-09 | Statically enforce that ULub is only between levels. | Gaëtan Gilbert | |
| 2018-03-09 | Option for messing with inference of irrelevant constraints | Gaëtan Gilbert | |
| 2018-03-09 | Cumulativity: 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-09 | Allow 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-09 | Merge PR #6480: Allow Prop as source for coercions | Maxime Dénès | |
| 2018-03-09 | Merge PR #6947: coqide: queries from the query window are routed there (fix ↵ | Maxime Dénès | |
| #5684) | |||
| 2018-03-09 | Adding a missing unification in typing.ml. | Hugo Herbelin | |
| 2018-03-09 | Merge PR #6818: Sphinx doc infrastructure | Maxime Dénès | |
| 2018-03-09 | Moving Gitlab CI documentation build to the main Coq build. | Maxime Dénès | |
| 2018-03-09 | Integration of a sphinx-based documentation generator. | Maxime Dénès | |
| The original contribution is from Clément Pit-Claudel. I updated his code and integrated it with the Coq build system. Many improvements by Paul Steckler (MIT). This commit adds the infrastructure but no content. | |||
| 2018-03-09 | Configure now fails with -with-doc yes when a doc dependency is missing. | Maxime Dénès | |
| 2018-03-09 | Merge PR #6895: [compat] Remove "Refolding Reduction" option. | Maxime Dénès | |
| 2018-03-09 | Merge PR #6820: Tacticals assert_fails and assert_succeeds | Maxime Dénès | |
| 2018-03-09 | Add an overlay for Equations and Ltac2. | Pierre-Marie Pédrot | |
| 2018-03-09 | Documenting the Export modifier for options in CHANGES. | Pierre-Marie Pédrot | |
| 2018-03-09 | Implement the Export Set/Unset feature. | Pierre-Marie Pédrot | |
| This feature has been asked many times by different people, and allows to have options in a module that are performed when this module is imported. This supersedes the well-numbered cursed PR #313. | |||
| 2018-03-09 | Export the various option localities in the API. | Pierre-Marie Pédrot | |
| This prevents relying on an underspecified bool option argument. | |||
| 2018-03-09 | doc and changes for coercion from prop/type | charguer | |
| 2018-03-09 | added test for coercion from type | charguer | |
| 2018-03-09 | allow Prop as source for coercions | charguer | |
| 2018-03-09 | Merge PR #6941: [toplevel] Respect COQ_COLORS environment variable | Maxime Dénès | |
| 2018-03-09 | Merge PR #6945: Fix error with univ binders on monomorphic records. | Maxime Dénès | |
| 2018-03-09 | Merge PR #6871: [build] Simpler byte/opt toplevel build. | Maxime Dénès | |
| 2018-03-09 | Merge PR #6155: Get rid of ' notation for Zpos in QArith | Maxime Dénès | |
| 2018-03-09 | Merge PR #6800: [checker] Printer cleanup. | Maxime Dénès | |
| 2018-03-09 | Merge PR #6747: Relax conversion of constructors according to the pCuIC model | Maxime Dénès | |
| 2018-03-09 | Merge PR #6328: Fix #6313: lost goals in nested ltac in refine | Maxime Dénès | |
| 2018-03-09 | Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec values | Maxime Dénès | |
| 2018-03-09 | Merge PR #6496: Generate typed generic code from ltac macros | Maxime Dénès | |
| 2018-03-09 | Merge PR #6937: Add empty compat file for Coq 8.8 | Maxime Dénès | |
| 2018-03-09 | Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for ↵ | Maxime Dénès | |
| fiat-crypto/OSX | |||
| 2018-03-08 | More examples about shelve/given_up in tactic-in-terms. | Hugo Herbelin | |
| 2018-03-08 | Cosmetic: add an expected newline in proof_global. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |