aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/plugin
AgeCommit message (Expand)Author
2018-07-31agressive fix for duplicated files!Cyril Cohen
2018-07-12Replace all the CoInductives with VariantsKazuhiko Sakaguchi
2018-04-20remove ssr plugin for 8.4 and 8.5Enrico Tassi
2018-03-21Declare prenex implicits for `Some_inj`Anton Trunov
2018-02-26Add ssrmatching.v transitional fileErik Martin-Dorel
2017-11-14Update v8.5 plugin to fix math-comp/math-comp#61Erik Martin-Dorel
2017-10-30Fix obsolete vernacular syntax for locality.Maxime Dénès
2017-06-09fix compilation on 8.5Enrico Tassi
2017-06-09fix compilation on 8.6Enrico Tassi
2017-06-07For trunk, use merged ssr plugin.Maxime Dénès
2017-06-06Fix plugin after Sigma removal.Maxime Dénès
2017-06-06Merge pull request #127 from herbelin/trunk+interp_closed_glob_constrMaxime Dénès
2017-05-31Adapting to PR #590 (a more explicit algebraic type for evars of kind Matchin...Hugo Herbelin
2017-05-31Binding glob_constr to interp_glob_closure so as to factorize low-level code.Hugo Herbelin
2017-05-25[coqlib] Update to explicitly build terms from references.Emilio Jesus Gallego Arias
2017-05-25Merge pull request #125 from ejgallego/options+remove_non_syncMaxime Dénès
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-17Coq PR #565: G_vernac.subgoal_command is replaced by query_commandGaetan Gilbert
2017-04-12Merge pull request #119 from maximedenes/econstrMaxime Dénès
2017-04-07[camplX] Remove camlp4 support.Emilio Jesus Gallego Arias
2017-04-05Merge remote-tracking branch 'upstream/master' into econstrMaxime Dénès
2017-04-04Fix ML compilation after introduction of EInstance.Pierre-Marie Pédrot
2017-04-03Adapt the ssr plugin to Coq's PR#417.Maxime Dénès
2017-03-24[econstr] Adapt to naming changes.Emilio Jesus Gallego Arias
2017-03-24Port to EConstrEnrico Tassi
2017-03-21Merge pull request #108 from ejgallego/pp_new_fixMaxime Dénès
2017-02-23[safe-string] Allow compilation with -safe-string.Emilio Jesus Gallego Arias
2017-02-21Use pp_with as msg_with is being removed upstream.Emilio Jesus Gallego Arias
2017-02-21Compatiblity with Ltac as a plugin.Maxime Dénès
2016-12-19fix compilation on 8.5Enrico Tassi
2016-12-06backport Coq PR#387 on ssrmatching for Coq v8.5Enrico Tassi
2016-12-06Use Tacred.unfoldn [AllOccurrences..] to work around Coq #5250Enrico Tassi
2016-12-06rewrite /primitive_projection is now supported (fix #85)Enrico Tassi
2016-11-08fix compilation on 8.6 and trunkEnrico Tassi
2016-11-07update copyright bannerAssia Mahboubi
2016-10-24removing the need of bracket to delimit ssrpatternargCyril Cohen
2016-10-12changing "ssreflect.ml4" so that we avoid triggering bugs in camlp5's "pr_o.c...Matej Kosik
2016-09-27Add a typing colon in the output of the Search ssreflect vernacular.Erik Martin-Dorel
2016-09-24Fix ML compilation after Ltac refactoring.Pierre-Marie Pédrot
2016-09-23FIX: compilation wrt. commit 9c35248 on Coq trunk branch.Matej Kosik
2016-09-22fix compilation wrt. commit 699b70c in Coq trunkMatej Kosik
2016-09-16Fix compilation after change in CErrors API.Pierre-Marie Pédrot
2016-08-26fix compilation wrt. commit 69388fc in Coq trunkMatej Kosik
2016-08-25FIX: adding missing version of the ssreflect plugin that compiles with Coq v8.6.Matej Kosik
2016-08-24Possible code compaction motivated by Enrico's remark: https://github.com/ma...Matej Kosik
2016-08-17Removing calls of "Context.Named.Declaration.to_tuple" functionMatej Kosik
2016-08-17use a convenient module alias instead of "Context.Rel.Declaration" and "Conte...Matej Kosik
2016-08-16fix compilation on trunk (thanks Matej)Enrico Tassi
2016-07-03Fix compilation after Errors and Closure were renamed.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:51:21 +0000