aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-03-17.gitignore (ssrmatching.v)Pierre-Yves Strub
2017-03-13Merge pull request #114 from strub/ignore-vioEnrico
2017-03-13Reflection lemmas for `seq.uniq`Pierre-Yves Strub
2017-03-13[gitignore]: ignore .vio filesPierre-Yves Strub
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-21Merge pull request #110 from maximedenes/ltac-pluginEnrico
2017-02-21Merge pull request #107 from ejgallego/travis+v8.5Enrico
2017-02-21Compatiblity with Ltac as a plugin.Maxime Dénès
2017-02-07[travis] Make v8.5 build againEmilio Jesus Gallego Arias
2017-02-07remove documentation for subfilter.Tanaka Akira
2017-02-07Merge pull request #105 from ejgallego/travisCyril Cohen
2017-02-07[travis] Build 70% of FT proof.Emilio Jesus Gallego Arias
2017-02-07[travis] Improve parallelism in build (cf #88)Emilio Jesus Gallego Arias
2017-02-06Build status in READMECyril Cohen
2017-02-06Merge pull request #103 from ejgallego/travisEnrico
2017-02-06[travis] Add initial Travis CI support.Emilio Jesus Gallego Arias
2017-02-04adding rquot_comRingTypeCyril Cohen
2017-01-18Merge pull request #78 from falcondai/patch-1Enrico
2016-12-20Merge pull request #87 from ybertot/masterAssia Mahboubi
2016-12-20correct a typo in the documentationYves Bertot
2016-12-19fix compilation on 8.5Enrico Tassi
2016-12-07better test for primitive projectionsEnrico Tassi
2016-12-07new test for "rewrite /x" when x is OpaqueEnrico Tassi
2016-12-06backport Coq PR#387 on ssrmatching for Coq v8.5Enrico Tassi
2016-12-06add test for unfolding primitive projectionsEnrico 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-17Merge pull request #82 from hivert/fixdocEnrico
2016-11-17Merge remote-tracking branch 'upstream/master' into fixdocFlorent Hivert
2016-11-16Fixes the doc of mxalgebraFlorent Hivert
2016-11-08fix compilation on 8.6 and trunkEnrico Tassi
2016-11-07update copyright bannerAssia Mahboubi
2016-10-25minor change to the opam install exampleFalcon Dai
2016-10-24removing the need of bracket to delimit ssrpatternargCyril Cohen
2016-10-24wip shorter proof dec factor theoremsCyril Cohen
2016-10-24better ltngtPCyril Cohen
2016-10-13Make: avoid >> Make, pass args to coq_makefile instead (#77)Enrico Tassi
2016-10-13Merge pull request #65 from gares/masterCyril Cohen
2016-10-13Merge pull request #66 from thery/masterCyril Cohen
2016-10-12Merge pull request #76 from matej-kosik/masterEnrico
2016-10-12changing "ssreflect.ml4" so that we avoid triggering bugs in camlp5's "pr_o.c...Matej Kosik
2016-10-05Generalization in the type of contra_eq/contra_neq.Assia Mahboubi
2016-09-28Merge pull request #69 from ejgallego/dont-depend-on-programCyril Cohen
2016-09-28Merge pull request #73 from erikmd/patch-searchEnrico
2016-09-27Add a typing colon in the output of the Search ssreflect vernacular.Erik Martin-Dorel
2016-09-26Merge pull request #72 from ppedrot/partial-fixEnrico
2016-09-24Fix ML compilation after Ltac refactoring.Pierre-Marie Pédrot
2016-09-23Merge pull request #71 from matej-kosik/masterEnrico
2016-09-23FIX: compilation wrt. commit 9c35248 on Coq trunk branch.Matej Kosik
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 21:42:32 +0000