| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-09-23 | FIX: compilation wrt. commit 9c35248 on Coq trunk branch. | Matej Kosik | |
| 2016-09-22 | fix compilation wrt. commit 699b70c in Coq trunk | Matej Kosik | |
| 2016-09-16 | Fix compilation after change in CErrors API. | Pierre-Marie Pédrot | |
| 2016-08-26 | fix compilation wrt. commit 69388fc in Coq trunk | Matej Kosik | |
| 2016-08-25 | FIX: adding missing version of the ssreflect plugin that compiles with Coq v8.6. | Matej Kosik | |
| The committed files represent copies of the ssreflect plugin for Coq trunk taken from commit c353aa5 which is the last commit in which ssreflect plugin marked for Coq trunk is usable with both, Coq trunk as well as Coq v8.6. | |||
| 2016-08-24 | Possible code compaction motivated by Enrico's remark: ↵ | Matej Kosik | |
| https://github.com/math-comp/math-comp/pull/58#discussion_r76048943 | |||
| 2016-08-17 | Removing calls of "Context.Named.Declaration.to_tuple" function | Matej Kosik | |
| 2016-08-17 | use a convenient module alias instead of "Context.Rel.Declaration" and ↵ | Matej Kosik | |
| "Context.Named.Declaration" | |||
| 2016-08-16 | fix compilation on trunk (thanks Matej) | Enrico Tassi | |
| 2016-07-03 | Fix compilation after Errors and Closure were renamed. | Maxime Dénès | |
| 2016-07-01 | Fix compilation after renaming of reduction functions and flags in Coq. | Maxime Dénès | |
| 2016-06-16 | Port build system to trunk (ssrmatching merged in Coq) | Enrico Tassi | |
| 2016-06-03 | fixing compilation (with Coq trunk & Coq v8.5) | Matej Kosik | |
| 2016-05-31 | Compatibility with latest Coq trunk. | Emilio Jesus Gallego Arias | |
| 2016-05-18 | Fix compilation after the change of API in Tactics. | Pierre-Marie Pédrot | |
| 2016-05-16 | Fix compilation after the renaming of Lexer into CLexer. | Pierre-Marie Pédrot | |
| 2016-05-09 | Fix compilation after the merge of the dynamic tactic value branch. | Pierre-Marie Pédrot | |
| 2016-05-02 | Fixing compilation after the merge of ML-tactic-notation branch. | Pierre-Marie Pédrot | |
| 2016-03-27 | Fixing ML compilation. | Pierre-Marie Pédrot | |
| 2016-03-03 | [search] Use msg_info to notify search results. | Emilio Jesus Gallego Arias | |
| By default, the search command calls `Pp.msg` to print search results. Unfortunately, this bypasses the `log_via_feedback` option and produces not very nice results on feedback-depending IDES like JsCoq. A proper fix would involve merging coq/coq#143 , and the upcoming search cleanup, but this should do the trick for now. I couldn't observe any problem with the usual testing. | |||
| 2016-03-02 | fix compilation of ssrmatching in trunk | Enrico Tassi | |
| 2016-02-25 | fix compilation | Enrico Tassi | |
| 2016-02-25 | ssrpattern: compose nicely with Tactic Notation | Enrico Tassi | |
| 2016-02-22 | Guard "catch all" exception handler using Errors.noncritical | Enrico Tassi | |
| 2016-02-22 | rewrite: matching do not instantiate goal evars | Enrico Tassi | |
| 2016-02-18 | typo in error message | thery | |
| 2016-02-18 | type in error message | thery | |
| 2016-02-15 | Removing compatibility layers. | Pierre-Marie Pédrot | |
| 2016-02-15 | Fixing ML compilation with trunk. | Pierre-Marie Pédrot | |
| 2016-02-03 | Register flag "SsrHave NoTCResolution" in the Summary (fix #6) | Enrico Tassi | |
| 2016-02-03 | resolve type classes under the correct set of univs (fix #22) | Enrico Tassi | |
| 2016-02-02 | fix compilation on 8.4 | Enrico Tassi | |
| 2016-02-02 | Do not hide critical errors with a blind catch all (fix #19) | Enrico Tassi | |
| 2016-02-02 | fix debug print | Enrico Tassi | |
| 2016-02-02 | Explicit error message if rewrite fails due to TC inference (fix #21) | Enrico Tassi | |
| 2016-02-01 | compilation on trunk fixed | Enrico Tassi | |
| 2016-01-31 | Partially fixing ML compilation on trunk. | Pierre-Marie Pédrot | |
| 2016-01-31 | half-repair compilation on trunk | Enrico Tassi | |
| 2016-01-12 | Move bullet initialization to ssreflect.v | Robbert Krebbers | |
| 2016-01-08 | fix version number in initialization message | Enrico Tassi | |
| 2015-12-04 | update license banner in .ml files | Enrico Tassi | |
| 2015-12-03 | Removing the only use of globTacticIn. | Pierre-Marie Pédrot | |
| 2015-12-03 | fix compilation on trunk (thanks PMP) | Enrico Tassi | |
| 2015-12-03 | fix: autogen + abstract variables clash | Enrico Tassi | |
| 2015-12-03 | fix: elim/v handles eliminator from Derive Inversion (issue #2) | Enrico Tassi | |
| Also: - fix elim trying to saturate too much and not raising the expected exn - fix fill_occ_pattern when occ is {-}, it used to lose the instantiation obtained by matching the term | |||
| 2015-12-03 | Add commands to trace the matching algorithm | Enrico Tassi | |
| 2015-12-03 | fix: Hint View is not a Query | Enrico Tassi | |
| 2015-09-27 | fix compilation on trunk | Enrico Tassi | |
| 2015-09-24 | Fix compilation on 8.5 | Enrico Tassi | |
| 2015-08-24 | Compare pattern heads (constants) up to "univs" | Enrico Tassi | |
| So that Universe Polymorphic constants are compared "correctly", i.e. not discriminated by the pattern filtering phase (verbatim head comparison) but eventually by unification. | |||
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |