| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-12-15 | Tentatively starting to use heuristics for evar-evar resolution: first | Hugo Herbelin | |
| step, prefer QuestionMark's to other evars, to comply with the filtering made on VarInstance, GoalEvar and QuestionMark for type class resolution. Maybe evars to be resolved by type class instances should eventually be marked with a specific tag. At least, this solves the current problem with compiling cancel2.v in LemmaOverloading. | |||
| 2014-12-15 | Failing on unbound notation variable in notation level modifiers | Hugo Herbelin | |
| + consequences of this check on the standard library (moved the no-op in Notation modifiers to what there were supposed to do; these are anyway local notations, so compatibility is safe - please AS or PL, amend if needed). | |||
| 2014-12-15 | New try on Fixing an evar_map bug revealed by commit 603b66f81 on | Hugo Herbelin | |
| unification flags (see also temporary revert in d083200ae5b). | |||
| 2014-12-15 | Tests for #3848 and #3854. | Hugo Herbelin | |
| 2014-12-15 | Documenting check_record + changing a possibly undefined int into int option. | Hugo Herbelin | |
| 2014-12-15 | About now accepts hypothesis names and goal selector. | Pierre Courtieu | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |