| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-12-15 | Fix treatment of universe context in typecheck inductive (was added | Matthieu Sozeau | |
| twice). Thanks to Marc Lasson for spotting this. | |||
| 2014-12-15 | Tests for Searchxxx commands added and modified. | Pierre Courtieu | |
| 2014-12-15 | Fixing bug #3865. | Pierre-Marie Pédrot | |
| 2014-12-14 | Util.un_op -> Option.default | Pierre Boutillier | |
| 2014-12-14 | Fix merging of name maps in union of universe contexts. | Matthieu Sozeau | |
| 2014-12-14 | Fixing bug #3858 and #3817 in one stroke. | Pierre-Marie Pédrot | |
| 2014-12-14 | Revert "Fixing bug #3817." | Pierre-Marie Pédrot | |
| This reverts commit ad2a0308b1592c7235714a2cca926f3b55accbb2. | |||
| 2014-12-12 | Add Ltac syntax for the [tclIFCATCH] primitive. | Arnaud Spiwack | |
| [tryif t then t2 else t3] behaves like [t;t2] if [t] has at least one success, or [t3] otherwise. It generalises [t||t3] as failures from [t2] will not be caught. | |||
| 2014-12-12 | Make sure the goals on the shelve are identified as goal and unresolvable ↵ | Arnaud Spiwack | |
| for typeclasses. This was not the case for goals created at the end of the tactic by salvaging the [future_goals] from the evar map. It would cause typeclass resolution to try and solve these goals (if they have a class type) at each subsequent tactic. Fixes #3841. | |||
| 2014-12-12 | Searchxxx now interpret patterns in goal environment if any. | Pierre Courtieu | |
| This makes such things work: x:nat h: x = 3 ================ True Search x. | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |