| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-09 | Merge PR #6775: Allow using cumulativity without forcing strict constraints. | Maxime Dénès | |
| 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 | |
| 2018-03-08 | A comment in Proofview.with_shelf. | Hugo Herbelin | |
| 2018-03-08 | Add an invariant on future goals in Proof.run_tactic. | Hugo Herbelin | |
| More precisely, we check that future goals retrieved in run_tactic have no given_up goals since given_up goals are supposed to be produced only by Proofview.given_up and put on the given_up store. Doing the same for the shelf does not work: there is a situation where run_tactic ends where the same goal is both in the comb and on the shelf. This is when calling "clear x" on a goal "x:A |- ?p:B(?q[x])" when the dependent goal "x:A |- ?q:C" is not on the shelf. Tactic "clear" creates "|- ?p':B(?q'[])" and "|- ?q':C". The "advance" thing sees that the new comb is now composed of ?p' and ?q' but ?q' is a future goal which is later collected on the shelf (which ?q' is also in the comb). I tried to remove this redundancy but apparently it is necessary. There is an example in HoTT (file Classes/theory/rational.v) which requires this redundancy. I did not investigate why: the dependent evar is created by ring as part of a big term. So, as a conclusion, I kept the redundancy. | |||
| 2018-03-08 | Add an invariant on given up goals in class_tactics. | Hugo Herbelin | |
| 2018-03-08 | Proof engine: support for nesting tactic-in-term within other tactics. | Hugo Herbelin | |
| Tactic-in-term can be called from within a tactic itself. We have to preserve the preexisting future_goals (if called from pretyping) and we have to inform of the existence of pending goals, using future_goals which is the only way to tell it in the absence of being part of an encapsulating proofview. This fixes #6313. Conversely, future goals, created by pretyping, can call ltac:(giveup) or ltac:(shelve), and this has to be remembered. So, we do it. | |||
| 2018-03-08 | Adding tclPUTGIVENUP/tclPUTSHELF in Proofview.Unsafe. | Hugo Herbelin | |
| Adding also tclSETSHELF/tclGETSHELF by consistency with tclSETGOALS/tclGETGOALS. However, I feel that this is too low-level to be exported as a "tcl". Doesn't a "tcl" mean that it is supposed to be used by common tactics? But is it reasonable that a common tactic can change and modify comb and shelf without passing by a level which e.g. checks that no goal is lost in the process. So, I would rather be in favor of removing tclSETGOALS/tclGETGOALS which are anyway aliases for Comb.get/Comb.set. Conversely, what is the right expected level of abstraction for proofview.ml? | |||
| 2018-03-08 | Add function bind in option.ml. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |