aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* Hconsing continuedGravatar Hugo Herbelin2015-08-02
* Fixing test apply.v (had wrong option name).Gravatar Hugo Herbelin2015-08-02
* Fixing pop_rel_contextGravatar Hugo Herbelin2015-08-02
* Documenting in passing.Gravatar Hugo Herbelin2015-08-02
* Hopefully clearer printing of stack when debugging evarconv unification.Gravatar Hugo Herbelin2015-08-02
* Failing when reaching end of file with unterminated comment whenGravatar Hugo Herbelin2015-08-02
* Cosmetic changes in evarconv.ml: hopefully more regular names and formGravatar Hugo Herbelin2015-08-02
* Cosmetic changes in evarconv.ml: hopefully more regular form andGravatar Hugo Herbelin2015-08-02
* Cosmetic changes in evarconv.ml: hopefully using better self-documenting names.Gravatar Hugo Herbelin2015-08-02
* Evarconv.ml: small cut-elimination, saving useless zip.Gravatar Hugo Herbelin2015-08-02
* Cosmetic in evarconv.ml: naming a local function for better readibility.Gravatar Hugo Herbelin2015-08-02
* Adding a notation { x & P } for { x : _ & P }.Gravatar Hugo Herbelin2015-08-02
* A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2015-08-02
* Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2015-08-02
* Give a way to control if the decidable-equality schemes are built likeGravatar Hugo Herbelin2015-08-02
* Removing the generalization of the body of inductive schemes fromGravatar Hugo Herbelin2015-08-02
* Fixing #4221 (interpreting bound variables using ltac env was possiblyGravatar Hugo Herbelin2015-08-02
* Granting Jason's request for an ad hoc compatibility option onGravatar Hugo Herbelin2015-08-02
* Documenting change of behavior of apply when the lemma is a tuple andGravatar Hugo Herbelin2015-08-02
* For convenience, making yes and on, and no and off synonymous inGravatar Hugo Herbelin2015-08-02
* Fix typos in the Extraction part of the reference manual.Gravatar Guillaume Melquiond2015-07-31
* Fix typos in the Micromega part of the reference manual.Gravatar Guillaume Melquiond2015-07-31
* Improve the table of content of the reference manual.Gravatar Guillaume Melquiond2015-07-31
* Remove some outdated files and fix permissions.Gravatar Guillaume Melquiond2015-07-31
* Followup of 9f81b58551.Gravatar Pierre-Marie Pédrot2015-07-30
* STM: make multiple, admitted, nested proofs work (fix #4314)Gravatar Enrico Tassi2015-07-30
* STM: emit a warning when a QED/Admitted proof contains a nested lemmaGravatar Enrico Tassi2015-07-30
* STM: fix backtrack in presence of nested, immediate, proofsGravatar Enrico Tassi2015-07-30
* STM: remove assertion not being true for nested, immediate, proofs (#4313)Gravatar Enrico Tassi2015-07-30
* Test file for bug #4289 (buggy hash-consing of kernel name pairsGravatar Hugo Herbelin2015-07-30
* Fixing bug #4289 (hash-consing only user part of constant notGravatar Hugo Herbelin2015-07-30
* A printer for printing constants of the env (maybe useful when there are not ...Gravatar Hugo Herbelin2015-07-30
* Avoid suggesting elim and decompose in the FAQ.Gravatar Guillaume Melquiond2015-07-30
* Remove some output of Qed in the FAQ.Gravatar Guillaume Melquiond2015-07-30
* Fix some broken Coq scripts in the documentation.Gravatar Guillaume Melquiond2015-07-30
* Fix width of underscore in coq_tex output.Gravatar Guillaume Melquiond2015-07-30
* Fix broken regexp.Gravatar Guillaume Melquiond2015-07-30
* Remove unused variables.Gravatar Guillaume Melquiond2015-07-30
* Remove usage of Printexc.catch in the tools, as it is deprecated since 2001.Gravatar Guillaume Melquiond2015-07-30
* Make coq-tex more robust with respect to the (non-)command on the last line.Gravatar Guillaume Melquiond2015-07-29
* Remove empty commands from the output of coq-tex.Gravatar Guillaume Melquiond2015-07-29
* Improve the FAQ a bit.Gravatar Guillaume Melquiond2015-07-29
* Rewrite the main loop of coq-tex.Gravatar Guillaume Melquiond2015-07-29
* Adding test for bug #3779.Gravatar Pierre-Marie Pédrot2015-07-29
* Fixing some English misspelling.Gravatar Hugo Herbelin2015-07-29
* Fixing what seems to be a typo.Gravatar Hugo Herbelin2015-07-29
* Fixing bug #3811: "Universe annotations confused inside generalizing binders".Gravatar Pierre-Marie Pédrot2015-07-29
* Adding a test for bug #4280.Gravatar Pierre-Marie Pédrot2015-07-28
* Fix for bug #4280: "decide equality produces terms that don't compute well".Gravatar Pierre-Marie Pédrot2015-07-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 21:35:50 +0000