| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-03 | Type@{_} should not produce a flexible algebraic universe. | Gaetan Gilbert | |
| Otherwise [(fun x => x) (Type : Type@{_})] becomes [(fun x : Type@{i+1} => x) (Type@{i} : Type@{i+1})] breaking the invariant that terms do not contain algebraic universes (at the lambda abstraction). | |||
| 2017-05-03 | Allow flexible anonymous universes in instances and sorts. | Gaetan Gilbert | |
| The addition to the test suite showcases the usage. | |||
| 2017-05-03 | Merge PR#411: Mention template polymorphism in the documentation. | Maxime Dénès | |
| 2017-05-03 | Fix outdated description in RefMan. | Théo Zimmermann | |
| 2017-05-02 | applied the patch for printing types of let bindings by @herbelin | Abhishek Anand (@brixpro-home) | |
| 2017-05-02 | Remove dead code in native compiler. | Maxime Dénès | |
| 2017-05-02 | Fix two new unused opens. | Maxime Dénès | |
| 2017-05-02 | Remove unused module definition after merging PR#592. | Maxime Dénès | |
| 2017-05-02 | Merge PR#592: Fix bug #5501: Universe polymorphism breaks proof involving auto. | Maxime Dénès | |
| 2017-05-02 | Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions ↵ | Maxime Dénès | |
| with evars). | |||
| 2017-05-02 | Merge PR#582: Fix warnings | Maxime Dénès | |
| 2017-05-02 | Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite files | Maxime Dénès | |
| 2017-05-02 | Merge PR#599: Repairing `Set Rewriting Schemes` | Maxime Dénès | |
| 2017-05-02 | Merge PR#596: Fix for bug 5507. Mispelt de Bruijn. | Maxime Dénès | |
| 2017-05-02 | Avoiding registering files from _build_ci when not calling Makefile.ci. | Hugo Herbelin | |
| 2017-05-02 | Merge PR#595: Avoiding registering files from _build_ci for computing ↵ | Maxime Dénès | |
| dependencies | |||
| 2017-05-01 | Add bmsherman/topology to the ci | Jason Gross | |
| This development of @bmsherman tests universe polymorphism and setoid rewriting in type, and should build with v8.6 and trunk. | |||
| 2017-05-01 | Fixing Set Rewriting Schemes bugs introduced in v8.5. | Hugo Herbelin | |
| - Fixing a typo introduced in 31dbba5f. - Adapting to computation of universe constraints in pretyping. - Adding a regression test. | |||
| 2017-05-01 | More consistent writing of de Bruijn. | Théo Zimmermann | |
| 2017-05-01 | remove unneeded -emacs flag to coq-prog-args | Paul Steckler | |
| 2017-05-01 | Removing dead code in Autorewrite. | Pierre-Marie Pédrot | |
| Since 260965d, an imperative code was semantically the identity because the closure allocation was not performed at the right moment. Because of it intricacy, I cannot really tell the original motivations of this piece of code, although it looks like it was for there for pretty-printing of errors. Anyway, both because the code was dubious and its effect not observed, it cannot hurt to remove it. | |||
| 2017-05-01 | Fixing #5487 (v8.5 regression on ltac-matching expressions with evars). | Hugo Herbelin | |
| The fix follows an invariant enforced in proofview.ml on the kind of evars that are goals or that occur in goals. One day, evar kinds will need a little cleaning... PS: This is a second attempt, completing db28e82 which was missing the case PEvar in constr_matching.ml. Indeed the attached fix to #5487 alone made #2602 failing, revealing that the real cause for #2602 was actually not fixed and that if the test for #2602 was working it was because of #5487 hiding the real problem in #2602. | |||
| 2017-05-01 | Really fixing #2602 which was wrongly working because of #5487 hiding the cause. | Hugo Herbelin | |
| The cause was a missing evar/evar clause in ltac pattern-matching function (constr_matching.ml). | |||
| 2017-05-01 | Fix for bug 5507. Mispelt de Bruijn. | Théo Zimmermann | |
| 2017-05-01 | Avoiding registering files from _build_ci when not calling Makefile.ci. | Hugo Herbelin | |
| 2017-05-01 | Answer to db28e827d: I did test the commit on test-suite but for some | Hugo Herbelin | |
| reason I overlooked the result, maybe a missing make clean. As for testing on the travis test architecture, I could have done it. This is a question of compromise. I was so certain that it would work that I did not test. And anyway, the travis test is not absolute either. In any case, I'm very sorry about the confusion it introduced. ~~~~ BY THE WAY, NO NEED TO SHOUT ~~~~ ~~~~ IT IS A BIG MISCONCEPTION ABOUT HUMAN BEINGS ~~~~ ~~~~ TO BELIEVE THAT THEY DO MISTAKES INTENTIONALLY ~~~~ Thank you! | |||
| 2017-04-30 | Functional choice <-> [inhabited] and [forall] commute | Gaetan Gilbert | |
| 2017-04-30 | Fix bug #5501: Universe polymorphism breaks proof involving auto. | Pierre-Marie Pédrot | |
| A universe substitution was lacking as the normalized evar map was dropped. | |||
| 2017-04-30 | Fixing "decide equality"'s bug #5449. | Hugo Herbelin | |
| The code was assuming that the terms t and u for which {t=u}+{t<>u} is proved were distinct. We refine an internal "generalize" of "u" so that it works on the two precise occurrences to abstract, even if other occurrences of u occur as subterm of t too. We also reuse the global constants found in the statement rather than reconstructing them (this seems better in case the global constants eventually get polymorphic universes?). | |||
| 2017-04-29 | Suppress warning message in stdlib. | Guillaume Melquiond | |
| 2017-04-28 | Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)." | Maxime Dénès | |
| One day I'll get bored of spending my nights fixing commits that were pushed without being tested, and I'll ask for removal of push rights. But for now let's pretend I haven't insisted enough: ~~~~ PLEASE TEST YOUR COMMITS BEFORE PUSHING ~~~~ Thank you! | |||
| 2017-04-28 | Revert "Renaming allow_patvar flag of intern_gen into pattern_mode." | Maxime Dénès | |
| This reverts commit 7bdfa1a4e46acf11d199a07bfca0bc59381874c3. | |||
| 2017-04-28 | Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"." | Maxime Dénès | |
| I'm sure this was pushed by accident, since testing shows immediately that it breaks the compilation of the ssreflect plugin, hence all developments relying on it in Travis. | |||
| 2017-04-28 | Allow interactive editing of {C,}Morphisms in PG | Jason Gross | |
| 2017-04-28 | Add .dir-locals.el and _CoqProject files for emacs stdlib editing | Jason Gross | |
| These set up PG to use the local coqtop, and the local coqlib, when editing files in the stdlib. As per https://github.com/coq/coq/pull/386#issuecomment-279012238, we can use `_CoqProject` for `theories/Init`, and this allows CoqIDE to edit those files. However, we cannot use it for `theories/`, because a `_CoqProject` file will override a `.dir-locals.el` in the same directory, and there is no way to get PG to pick up a valid `-coqlib` from `_CoqProject` (because it'll take the path relative to the current directory, not relative to the directory of `_CoqProject`). | |||
| 2017-04-28 | Using a more explicit algebraic type for evars of kind "MatchingVar". | Hugo Herbelin | |
| A priori considered to be a good programming style. | |||
| 2017-04-28 | Renaming allow_patvar flag of intern_gen into pattern_mode. | Hugo Herbelin | |
| This highlights that this is a binary mode changing the interpretation of "?x" rather than additionally allowing patvar. | |||
| 2017-04-28 | Fixing #5487 (v8.5 regression on ltac-matching expressions with evars). | Hugo Herbelin | |
| The fix follows an invariant enforced in proofview.ml on the kind of evars that are goals or that occur in goals. One day, evar kinds will need a little cleaning... | |||
| 2017-04-28 | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵ | Maxime Dénès | |
| let-ins | |||
| 2017-04-27 | Post-rebase warnings (unused opens and 2 unused values) | Gaetan Gilbert | |
| 2017-04-27 | Enable more warnings, and add -warn-error configure flag | Gaetan Gilbert | |
| 2017-04-27 | Fix 4.04 warnings | Gaetan Gilbert | |
| 2017-04-27 | Remove uses of [Flags.make_silent] | Gaetan Gilbert | |
| 2017-04-27 | Warning 29: non escaped end of line may be non portable | Gaetan Gilbert | |
| 2017-04-27 | Remove unused [open] statements | Gaetan Gilbert | |
| 2017-04-27 | Micromega: do not use Filename.temp_dir_path, remove unused values | Gaetan Gilbert | |
| 2017-04-27 | Remove unused constructors | Gaetan Gilbert | |
| 2017-04-27 | Add [_] prefix to unused values which maybe should be kept | Gaetan Gilbert | |
| 2017-04-27 | Remove some unused values and types | Gaetan Gilbert | |
| 2017-04-27 | Rename Sos_lib.(||) -> parser_or to avoid (deprecated) Pervasives.or | Gaetan Gilbert | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |