aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-08-29Adding a proof of surjective pairing on vectors.Hugo Herbelin
2015-08-29Fixing generation of dev/printers.mllib.d after ocamllibdep is used (48d611ff...Hugo Herbelin
2015-08-26Replacing old-style preferences in CoqIDE.Pierre-Marie Pédrot
2015-08-22Documenting the Shrink Abstract option.Pierre-Marie Pédrot
2015-08-22Allowing the abstract tactical to clear the environment from unused variables.Pierre-Marie Pédrot
2015-08-22Merge branch 'v8.5'Pierre-Marie Pédrot
2015-08-21Fixing #4318 (anomaly when applying args to a recursive notation in patterns).Hugo Herbelin
2015-08-19Removing code duplication in Lemmas.Pierre-Marie Pédrot
2015-08-19Documentation by giving a name to a large type.Pierre-Marie Pédrot
2015-08-17Highlighting of the "Next Obligation" command in CoqIDE.Pierre-Marie Pédrot
2015-08-17windows build scripts made more accurate in detecting failuresEnrico Tassi
2015-08-17Remove duplicate code.Guillaume Melquiond
2015-08-17Remove generatable documentation files from repository. (Fix bug #4315)Guillaume Melquiond
2015-08-16Using the new preference mechanism for colors in CoqIDE.Pierre-Marie Pédrot
2015-08-16Taking advantage of the new type of preferences.Pierre-Marie Pédrot
2015-08-16Turning CoqIDE preferences into new style.Pierre-Marie Pédrot
2015-08-16Simplifying CoqIDE preferences mechanism.Pierre-Marie Pédrot
2015-08-15Revert the four previous commits and update the description of Richpp.Pierre-Marie Pédrot
2015-08-15More invariants in Richpp.Pierre-Marie Pédrot
2015-08-15More parametric type for generalized XML.Pierre-Marie Pédrot
2015-08-15Statically ensure that we omit null annotations in Richpp.Pierre-Marie Pédrot
2015-08-15Fixing richpp behaviour w.r.t. its specification.Pierre-Marie Pédrot
2015-08-13report the full module path when reporting errors in coqdepGregory Malecha
2015-08-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-08-03Test file for #4254: Mutual inductives with parameters on Type raises anomaly.Maxime Dénès
2015-08-02Continuing 817308ab (use ltac env for terms in ltac context) + fixHugo Herbelin
2015-08-02Fixing test apply.v (had wrong option name).Hugo Herbelin
2015-08-02Fixing pop_rel_context.Hugo Herbelin
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Hconsing continuedHugo Herbelin
2015-08-02Fixing test apply.v (had wrong option name).Hugo Herbelin
2015-08-02Fixing pop_rel_contextHugo Herbelin
2015-08-02Documenting in passing.Hugo Herbelin
2015-08-02Hopefully clearer printing of stack when debugging evarconv unification.Hugo Herbelin
2015-08-02Failing when reaching end of file with unterminated comment whenHugo Herbelin
2015-08-02Cosmetic changes in evarconv.ml: hopefully more regular names and formHugo Herbelin
2015-08-02Cosmetic changes in evarconv.ml: hopefully more regular form andHugo Herbelin
2015-08-02Cosmetic changes in evarconv.ml: hopefully using better self-documenting names.Hugo Herbelin
2015-08-02Evarconv.ml: small cut-elimination, saving useless zip.Hugo Herbelin
2015-08-02Cosmetic in evarconv.ml: naming a local function for better readibility.Hugo Herbelin
2015-08-02Adding a notation { x & P } for { x : _ & P }.Hugo Herbelin
2015-08-02A patch renaming equal into eq in the module dealing withHugo Herbelin
2015-08-02Adding eq/compare/hash for syntactic view atHugo Herbelin
2015-08-02Give a way to control if the decidable-equality schemes are built likeHugo Herbelin
2015-08-02Removing the generalization of the body of inductive schemes fromHugo Herbelin
2015-08-02Fixing #4221 (interpreting bound variables using ltac env was possiblyHugo Herbelin
2015-08-02Granting Jason's request for an ad hoc compatibility option onHugo Herbelin
2015-08-02Documenting change of behavior of apply when the lemma is a tuple andHugo Herbelin
2015-08-02For convenience, making yes and on, and no and off synonymous inHugo Herbelin
2015-07-31Fix typos in the Extraction part of the reference manual.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 12:36:09 +0000