| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-12-12 | #4843 part 2 : The .cmxs files for plug-ins must have execute permission | Pierre Boutillier | |
| 2014-12-12 | Fix #3163 and #3843 part 1 : Cygwin DLLs have extension ".so", not ".dll" | Pierre Boutillier | |
| 2014-12-12 | Fix #3800 : cmxs need execution priviledges under windows | Pierre Boutillier | |
| 2014-12-12 | An option SimplIsCbn | Pierre Boutillier | |
| 2014-12-12 | Extend the syntax of simpl with a delta flag. | Arnaud Spiwack | |
| You can write 'simpl -[plus minus] div2'. Simpl does not use it for now. | |||
| 2014-12-12 | Searchxxx now search also the hypothesis and support goal selector. | Pierre Courtieu | |
| Documentation also updated. | |||
| 2014-12-12 | Two fixes in unification (bugs #3782 and #3709) | Matthieu Sozeau | |
| - In evarconv, check_conv_record properly computes the parameters of primitive record projections for later unification, adding env and sigma as arguments. - In unification, backtrack on pattern-unification and not only application unification if eta for a record failed. | |||
| 2014-12-12 | In discrimination nets, do not index lambdas if they're part of a beta | Matthieu Sozeau | |
| redex. | |||
| 2014-12-11 | handling Functional Scheme for required but not imported modules | Julien Forest | |
| 2014-12-11 | List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs) | Pierre Letouzey | |
| 2014-12-11 | First series of results on lists. | Sébastien Hinderer | |
| 2014-12-11 | Commit not ready. Sorry. | Hugo Herbelin | |
| Revert "Fixing an evar_map bug revealed by commit 603b66f81 on unification flags." This reverts commit d083200ae5b391ceffaa0329a8e3a334036c7968. | |||
| 2014-12-11 | Added a CannotSolveConstraint unification error and made experiments | Hugo Herbelin | |
| in reporting the chain of causes when unification fails. | |||
| 2014-12-11 | Fine-tuning unification error (using OccurCheck in evarconv). | Hugo Herbelin | |
| 2014-12-11 | Tentatively more informative report of failure when inferring | Hugo Herbelin | |
| pattern-matching predicate. | |||
| 2014-12-11 | Fixing an evar_map bug revealed by commit 603b66f81 on unification flags. | Hugo Herbelin | |
| This fixes current failure of RelationAlgebra. | |||
| 2014-12-11 | Test suite: keep message in sync with actual file deletions. | Xavier Clerc | |
| 2014-12-11 | Ignore *.vi files, just like *.vo files. | Xavier Clerc | |
| 2014-12-11 | New reproduction cases for the test suite. | Xavier Clerc | |
| 2014-12-10 | Fix dummy argument use in guess_elim: there are some cases where X_ind | Matthieu Sozeau | |
| is not defined while X_rect is, for example in HoTT/Coq. | |||
| 2014-12-10 | Revert commit that inverted the preference for FFlex/FProj problems in | Matthieu Sozeau | |
| kernel reduction. | |||
| 2014-12-10 | Fixing orientation of postponed subtyping problems. | Hugo Herbelin | |
| In the case of conversion, postponing by preserving the initial orientation. Was wrong from its initial version in Jan 2014, but was not visible because evar-evar subtyping was approximated by evar-evar conversion. Thanks to Enrico for a very short example highlighting the problem. In particular, this fixes Ergo. | |||
| 2014-12-10 | Using a more aggressive test for resolving pattern equations ?n = ?p: | Hugo Herbelin | |
| test pattern-unification after restriction of the evars so as to succeed earlier (no observational changes however in the examples at my disposal). | |||
| 2014-12-10 | typo | Enrico Tassi | |
| 2014-12-10 | test-suite: few tests for ".v -> .vi -> .vo" compilation chain | Enrico Tassi | |
| 2014-12-09 | Setup hook to change the unification algorithm used by evarconv, | Matthieu Sozeau | |
| e.g. for MTac. | |||
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | |
| 2014-12-09 | refman: switch all source files to utf8 | Pierre Letouzey | |
| Putting utf8 everywhere helps the maintainance of the online refman. And anyway, this is the way to go. We should also chase and migrate the few remaining iso-latin-1 files elsewhere in the sources. | |||
| 2014-12-09 | refman: fix broken urls | Pierre Letouzey | |
| 2014-12-09 | refman: remove ?uri=referer in urls pointing to validator.w3.org | Pierre Letouzey | |
| Unfortunately, these ?uri=referer parameters do not work correctly now that coq.inria.fr forces the switch to https before answering any document. See: http://validator.w3.org/docs/help.html#faq-referer I currently see no workaround for that, apart from generating links like ?uri=http://the.real.url/of/my/page, which would be quite painful. For now, users interested in checking the validity of our pages will have to copy-paste the url they want to check after clicking on the validator button. | |||
| 2014-12-09 | refman/Omega.tex: do not advertize Pierre Cregut's email for bug reports | Pierre Letouzey | |
| 2014-12-09 | refman/coqdoc.tex: fix two erroneous \url | Pierre Letouzey | |
| 2014-12-09 | refman: for xhtml validity, add 'alt' attributes to img | Pierre Letouzey | |
| 2014-12-09 | refman: avoid label names with whitespace (unsupported in html) | Pierre Letouzey | |
| 2014-12-09 | refman: xhtml validity of the cover page | Pierre Letouzey | |
| 2014-12-09 | coqdoc.css: fix a few errors | Pierre Letouzey | |
| 2014-12-09 | coqdoc: fix a few issues with xhtml validity (backport 1636f7 and 754abf1 ↵ | Pierre Letouzey | |
| from v8.4) - For the style of identifiers, coqdoc was using a 'type' attribute of tag <span>. But this attribute isn't a legal attribute of tag <span> according to the xhtml norm. Instead, I propose to use 'title' for that. The coqdoc.css now supports both approaches. - The names of inner links (cross references #foo) were containing arbitrary characters (in the case of a notation string). For instance in Utf8_core : <a name=":type_scope:'∀'_x_'..'_x_','_x"> Instead, when strange characters are detected, we now hash the string via Digest, and use this hexa hash as html label. - And some whitespace before /> | |||
| 2014-12-09 | doc/stdlib: fix the xhtml validity of the index-list template | Pierre Letouzey | |
| 2014-12-09 | doc: improved xhtml compatibility (cover, header,...) | Pierre Letouzey | |
| 2014-12-09 | doc/stdlib: fix the html charset in header.html and co | Pierre Letouzey | |
| 2014-12-09 | doc: version number in cover.html + updates in coq.inria.fr style | Pierre Letouzey | |
| To be continued someday, those style files are full of redundancies... | |||
| 2014-12-09 | Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la ↵ | notin | |
| documentation en ligne) | |||
| 2014-12-09 | Port to trunk the old commit r14895 of v8.4 (styles for the stdlib ↵ | notin | |
| documentation) This commit r14895 comes apparently itself from commit r12010 in branch v8.2 | |||
| 2014-12-08 | Fixing wrong evar_map in return clause inference, revealed by 48509b611. | Hugo Herbelin | |
| 2014-12-08 | Improved criterion for evar restriction in the configuration | Hugo Herbelin | |
| ?n[...] = ?p[...;x:=?n[...];...]. Indeed, x could be a solution for ?p. | |||
| 2014-12-08 | This is for documenting and slightly fixing commits 547e97e, c52aea7, 9a34d3e. | Hugo Herbelin | |
| As their commit messages suggested it, these commits were not intended to be committed at this time. They are part of a on-going merge of the code of induction and functional induction. Together with the fix here, they are supposingly transparent, semantically speaking. | |||
| 2014-12-08 | Closing bug 3837 | Julien Forest | |
| 2014-12-08 | Constructor tactics backtracking is done using [Tacticals.New] rather than ↵ | Arnaud Spiwack | |
| [Proofview]. The primitives in [Tacticals] respect Ltac's error level, whereas the one in [Proofview] do not necessarily. In that case the error caught was ignored causing arbitrary error level after [constructor] to be canceled. Needed the addition of an [ORD] variant to [OR] in [Tacticals.New] to avoid unnecessary precomputation (the 'D' stands for 'delay'). Fixes #3838. | |||
| 2014-12-07 | Step 4 : atomize_then | Hugo Herbelin | |
| 2014-12-07 | Step 2 | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |