| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-06-09 | fix compilation on 8.6 | Enrico Tassi | |
| 2017-06-07 | Merge pull request #129 from maximedenes/ssr-merge | Maxime Dénès | |
| Ssr merge | |||
| 2017-06-07 | Change failing test. | Maxime Dénès | |
| 2017-06-07 | For trunk, use merged ssr plugin. | Maxime Dénès | |
| 2017-06-06 | Merge pull request #128 from maximedenes/remove-sigma | Maxime Dénès | |
| Fix plugin after Sigma removal. | |||
| 2017-06-06 | Fix plugin after Sigma removal. | Maxime Dénès | |
| 2017-06-06 | Merge pull request #127 from herbelin/trunk+interp_closed_glob_constr | Maxime Dénès | |
| Binding glob_constr to interp_glob_closure so as to factorize low-level code. | |||
| 2017-06-05 | Merge pull request #123 from herbelin/trunk+pr590-patvar | Maxime Dénès | |
| Adapting to PR #590 (a more explicit algebraic type for evars of kind… | |||
| 2017-05-31 | Adapting to PR #590 (a more explicit algebraic type for evars of kind ↵ | Hugo Herbelin | |
| MatchingVar). | |||
| 2017-05-31 | Binding glob_constr to interp_glob_closure so as to factorize low-level code. | Hugo Herbelin | |
| 2017-05-28 | Merge pull request #126 from ejgallego/coqlib-part-02 | Maxime Dénès | |
| [coqlib] Update to explicitly build terms from references. | |||
| 2017-05-25 | [coqlib] Update to explicitly build terms from references. | Emilio Jesus Gallego Arias | |
| See coq/coq#678 | |||
| 2017-05-25 | Merge pull request #125 from ejgallego/options+remove_non_sync | Maxime Dénès | |
| [options] Sync with upstream API changes. | |||
| 2017-05-25 | Merge pull request #124 from ejgallego/located_switch | Maxime Dénès | |
| [ast] Adapt to Coq's #402 new generic AST node. | |||
| 2017-05-23 | [options] Sync with upstream API changes. | Emilio Jesus Gallego Arias | |
| 2017-04-19 | [ast] Adapt to Coq's #402 new generic AST node. | Emilio Jesus Gallego Arias | |
| 2017-04-17 | Merge pull request #120 from SkySkimmer/remove-vernacerror | Enrico | |
| Coq PR #565: G_vernac.subgoal_command is replaced by query_command | |||
| 2017-04-17 | Coq PR #565: G_vernac.subgoal_command is replaced by query_command | Gaetan Gilbert | |
| 2017-04-12 | Merge pull request #119 from maximedenes/econstr | Maxime Dénès | |
| Econstr support | |||
| 2017-04-07 | Merge pull request #113 from ejgallego/no_camlp4_compat | Maxime Dénès | |
| [camplX] Remove camlp4 support. | |||
| 2017-04-07 | [camplX] Remove camlp4 support. | Emilio Jesus Gallego Arias | |
| Adapting to Coq upstream. | |||
| 2017-04-05 | Merge remote-tracking branch 'upstream/master' into econstr | Maxime Dénès | |
| 2017-04-04 | Merge pull request #1 from ppedrot/econstr | Maxime Dénès | |
| Fix ML compilation after introduction of EInstance. | |||
| 2017-04-04 | Fix ML compilation after introduction of EInstance. | Pierre-Marie Pédrot | |
| 2017-04-03 | Merge pull request #118 from maximedenes/coq-pr417-landing | Enrico | |
| Adapt the ssr plugin to Coq's PR#417. | |||
| 2017-04-03 | Adapt the ssr plugin to Coq's PR#417. | Maxime Dénès | |
| Let-ins in constrexpr and glob_constr now take an optional type, instead of relying on a cast in the body. | |||
| 2017-03-24 | [econstr] Adapt to naming changes. | Emilio Jesus Gallego Arias | |
| 2017-03-24 | Port to EConstr | Enrico Tassi | |
| 2017-03-23 | ssrtest/elim.v: don't depend on Function | Enrico Tassi | |
| We inline the lemmas it generated, to ectly test the same thing as before. | |||
| 2017-03-21 | Merge pull request #108 from ejgallego/pp_new_fix | Maxime Dénès | |
| Use pp_with as msg_with is being removed upstream. | |||
| 2017-03-21 | Merge pull request #111 from ejgallego/safe_string | Enrico | |
| Compile with -safe-string | |||
| 2017-03-17 | Merge pull request #117 from strub/ignore-ssrmatching | Enrico | |
| .gitignore (ssrmatching.v) | |||
| 2017-03-17 | .gitignore (ssrmatching.v) | Pierre-Yves Strub | |
| 2017-03-13 | Merge pull request #114 from strub/ignore-vio | Enrico | |
| [gitignore]: ignore .vio files | |||
| 2017-03-13 | Reflection lemmas for `seq.uniq` | Pierre-Yves Strub | |
| 2017-03-13 | [gitignore]: ignore .vio files | Pierre-Yves Strub | |
| 2017-02-23 | [safe-string] Allow compilation with -safe-string. | Emilio Jesus Gallego Arias | |
| The first part of changes is easy, we could maybe polish the notation part a bit more. | |||
| 2017-02-21 | Use pp_with as msg_with is being removed upstream. | Emilio Jesus Gallego Arias | |
| 2017-02-21 | Merge pull request #110 from maximedenes/ltac-plugin | Enrico | |
| Compatiblity with Ltac as a plugin. | |||
| 2017-02-21 | Merge pull request #107 from ejgallego/travis+v8.5 | Enrico | |
| [travis] Make v8.5 build again | |||
| 2017-02-21 | Compatiblity with Ltac as a plugin. | Maxime Dénès | |
| 2017-02-07 | [travis] Make v8.5 build again | Emilio Jesus Gallego Arias | |
| We also remove PFsection6 from build as it seems to be too close. | |||
| 2017-02-07 | remove documentation for subfilter. | Tanaka Akira | |
| subfilter was exist at ssreflect-1.1 and removed at ssreflect-1.2. | |||
| 2017-02-07 | Merge pull request #105 from ejgallego/travis | Cyril Cohen | |
| [travis] Enable build of 70% of Feith-Thompsom proof | |||
| 2017-02-07 | [travis] Build 70% of FT proof. | Emilio Jesus Gallego Arias | |
| I'm afraid we cannot reliably build more with the 50 minutes timeout. | |||
| 2017-02-07 | [travis] Improve parallelism in build (cf #88) | Emilio Jesus Gallego Arias | |
| 2017-02-06 | Build status in README | Cyril Cohen | |
| 2017-02-06 | Merge pull request #103 from ejgallego/travis | Enrico | |
| [travis] Add initial Travis CI support. | |||
| 2017-02-06 | [travis] Add initial Travis CI support. | Emilio Jesus Gallego Arias | |
| 2017-02-04 | adding rquot_comRingType | Cyril Cohen | |
 |
index : coq-mathcomp | |
| Library of mathematical components formalized in Coq |
| aboutsummaryrefslogtreecommitdiff |