aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2016-09-22Merge pull request #70 from matej-kosik/masterEnrico
2016-09-22fix compilation wrt. commit 699b70c in Coq trunkMatej Kosik
2016-09-20[field] Remove unnecessary `Program Definition`Emilio Jesus Gallego Arias
2016-09-19Merge pull request #67 from ppedrot/partial-fixEnrico
2016-09-16Refactoring of binonialthery
2016-09-16Fix compilation after change in CErrors API.Pierre-Marie Pédrot
2016-09-07fix commentEnrico
2016-09-07abstract_context utility lemmaEnrico
2016-08-28Merge pull request #60 from matej-kosik/masterEnrico
2016-08-26fix compilation wrt. commit 69388fc in Coq trunkMatej Kosik
2016-08-25Merge pull request #59 from matej-kosik/masterEnrico
2016-08-25FIX: adding missing version of the ssreflect plugin that compiles with Coq v8.6.Matej Kosik
2016-08-25Factor theorem for decidable fields, (inspired by PY Strub)Cyril Cohen
2016-08-25Enriched numClosedFieldType so that it factors a lot of theory from both comp...Cyril Cohen
2016-08-24Merge pull request #58 from matej-kosik/masterEnrico
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
2016-07-01Fix compilation after renaming of reduction functions and flags in Coq.Maxime Dénès
2016-06-17fix parsing (coq trunk goal selector/ltac:)Enrico Tassi
2016-06-17this test is now in Coq, removing it.Enrico Tassi
2016-06-16Port build system to trunk (ssrmatching merged in Coq)Enrico Tassi
2016-06-03Merge pull request #49 from matej-kosik/masterEnrico
2016-06-03fixing compilation (with Coq trunk & Coq v8.5)Matej Kosik
2016-06-01Merge pull request #48 from ejgallego/pp_cleanup_fixEnrico
2016-05-31Compatibility with latest Coq trunk.Emilio Jesus Gallego Arias
2016-05-18Merge pull request #46 from ppedrot/partial-fixEnrico
2016-05-18Fix compilation after the change of API in Tactics.Pierre-Marie Pédrot
2016-05-16Merge pull request #44 from ppedrot/partial-fixEnrico
2016-05-16Fix compilation after the renaming of Lexer into CLexer.Pierre-Marie Pédrot
2016-05-12Merge pull request #43 from hivert/fixdocGeorges Gonthier
2016-05-12Fixes doc of mxrepresentation.vFlorent Hivert
2016-05-09Merge pull request #42 from ppedrot/partial-fixEnrico
2016-05-09Fix compilation after the merge of the dynamic tactic value branch.Pierre-Marie Pédrot
2016-05-04Merge pull request #40 from ppedrot/partial-fixEnrico
2016-05-02Fixing compilation after the merge of ML-tactic-notation branch.Pierre-Marie Pédrot
2016-04-15Merge pull request #39 from ppedrot/partial-fixEnrico
2016-04-08Fixing compilation after the merge of PR trunk-function_scope.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 05:02:36 +0000