| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-03 | Allowing to pass arbitrary data in internalization environments. | Pierre-Marie Pédrot | |
| 2017-05-03 | Exporting Nametab generic API. | Pierre-Marie Pédrot | |
| 2017-05-03 | Merge PR#541: Fixing "decide equality" bug #5449 | Maxime Dénès | |
| 2017-05-03 | Merge PR#588: Allow interactive editing of {C,}Morphisms in PG | Maxime Dénès | |
| 2017-05-03 | Merge PR#386: Better editing of the standard library in coqtop/PG | Maxime Dénès | |
| 2017-05-03 | Merge PR#602: Fix more warnings | Maxime Dénès | |
| 2017-05-03 | Merge PR#404: patch for printing types of let bindings | Maxime Dénès | |
| 2017-05-03 | Merge PR#411: Mention template polymorphism in the documentation. | Maxime Dénès | |
| 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#582: Fix warnings | Maxime Dénès | |
| 2017-05-02 | Merge PR#596: Fix for bug 5507. Mispelt de Bruijn. | Maxime Dénès | |
| 2017-05-02 | Merge PR#595: Avoiding registering files from _build_ci for computing ↵ | Maxime Dénès | |
| dependencies | |||
| 2017-05-01 | More consistent writing of de Bruijn. | Théo Zimmermann | |
| 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-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 "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 | 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 | |
| 2017-04-27 | Disambiguate Polynomial.Hyp and Mfourier.Hyp -> Assum | Gaetan Gilbert | |
| 2017-04-27 | Use [method!] to override methods (warning 7) | Gaetan Gilbert | |
| 2017-04-27 | Fix omitted labels in function calls | Gaetan Gilbert | |
| 2017-04-27 | Remove unused [rec] keywords | Gaetan Gilbert | |
| 2017-04-27 | Locally disable some warnings. | Gaetan Gilbert | |
| 2017-04-27 | Merge PR#414: Some more theory on powerRZ. | Maxime Dénès | |
| 2017-04-27 | Merge PR#583: [toplevel] More work on error handling. | Maxime Dénès | |
| 2017-04-27 | Merge PR#586: trivial cleanup commits which does not change Coq API | Maxime Dénès | |
| 2017-04-27 | Merge PR#568: Remove tactic compatibility layer | Maxime Dénès | |
| 2017-04-27 | Document the API changes. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |