aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Util.un_op -> Option.defaultGravatar Pierre Boutillier2014-12-14
* Fix merging of name maps in union of universe contexts.Gravatar Matthieu Sozeau2014-12-14
* Fixing bug #3858 and #3817 in one stroke.Gravatar Pierre-Marie Pédrot2014-12-14
* Revert "Fixing bug #3817."Gravatar Pierre-Marie Pédrot2014-12-14
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
* Make sure the goals on the shelve are identified as goal and unresolvable for...Gravatar Arnaud Spiwack2014-12-12
* Searchxxx now interpret patterns in goal environment if any.Gravatar Pierre Courtieu2014-12-12
* #4843 part 2 : The .cmxs files for plug-ins must have execute permissionGravatar Pierre Boutillier2014-12-12
* Fix #3163 and #3843 part 1 : Cygwin DLLs have extension ".so", not ".dll"Gravatar Pierre Boutillier2014-12-12
* Fix #3800 : cmxs need execution priviledges under windowsGravatar Pierre Boutillier2014-12-12
* An option SimplIsCbnGravatar Pierre Boutillier2014-12-12
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
* Two fixes in unification (bugs #3782 and #3709)Gravatar Matthieu Sozeau2014-12-12
* In discrimination nets, do not index lambdas if they're part of a betaGravatar Matthieu Sozeau2014-12-12
* handling Functional Scheme for required but not imported modulesGravatar Julien Forest2014-12-11
* List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)Gravatar Pierre Letouzey2014-12-11
* First series of results on lists.Gravatar Sébastien Hinderer2014-12-11
* Commit not ready. Sorry.Gravatar Hugo Herbelin2014-12-11
* Added a CannotSolveConstraint unification error and made experimentsGravatar Hugo Herbelin2014-12-11
* Fine-tuning unification error (using OccurCheck in evarconv).Gravatar Hugo Herbelin2014-12-11
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Fixing an evar_map bug revealed by commit 603b66f81 on unification flags.Gravatar Hugo Herbelin2014-12-11
* Test suite: keep message in sync with actual file deletions.Gravatar Xavier Clerc2014-12-11
* Ignore *.vi files, just like *.vo files.Gravatar Xavier Clerc2014-12-11
* New reproduction cases for the test suite.Gravatar Xavier Clerc2014-12-11
* Fix dummy argument use in guess_elim: there are some cases where X_indGravatar Matthieu Sozeau2014-12-10
* Revert commit that inverted the preference for FFlex/FProj problems inGravatar Matthieu Sozeau2014-12-10
* Fixing orientation of postponed subtyping problems.Gravatar Hugo Herbelin2014-12-10
* Using a more aggressive test for resolving pattern equations ?n = ?p:Gravatar Hugo Herbelin2014-12-10
* typoGravatar Enrico Tassi2014-12-10
* test-suite: few tests for ".v -> .vi -> .vo" compilation chainGravatar Enrico Tassi2014-12-10
* Setup hook to change the unification algorithm used by evarconv,Gravatar Matthieu Sozeau2014-12-09
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* refman: switch all source files to utf8Gravatar Pierre Letouzey2014-12-09
* refman: fix broken urlsGravatar Pierre Letouzey2014-12-09
* refman: remove ?uri=referer in urls pointing to validator.w3.orgGravatar Pierre Letouzey2014-12-09
* refman/Omega.tex: do not advertize Pierre Cregut's email for bug reportsGravatar Pierre Letouzey2014-12-09
* refman/coqdoc.tex: fix two erroneous \urlGravatar Pierre Letouzey2014-12-09
* refman: for xhtml validity, add 'alt' attributes to imgGravatar Pierre Letouzey2014-12-09
* refman: avoid label names with whitespace (unsupported in html)Gravatar Pierre Letouzey2014-12-09
* refman: xhtml validity of the cover pageGravatar Pierre Letouzey2014-12-09
* coqdoc.css: fix a few errorsGravatar Pierre Letouzey2014-12-09
* coqdoc: fix a few issues with xhtml validity (backport 1636f7 and 754abf1 fro...Gravatar Pierre Letouzey2014-12-09
* doc/stdlib: fix the xhtml validity of the index-list templateGravatar Pierre Letouzey2014-12-09
* doc: improved xhtml compatibility (cover, header,...)Gravatar Pierre Letouzey2014-12-09
* doc/stdlib: fix the html charset in header.html and coGravatar Pierre Letouzey2014-12-09
* doc: version number in cover.html + updates in coq.inria.fr styleGravatar Pierre Letouzey2014-12-09
* Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la document...Gravatar notin2014-12-09
* Port to trunk the old commit r14895 of v8.4 (styles for the stdlib documentat...Gravatar notin2014-12-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-18 17:50:38 +0000