aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-06-09fix compilation on 8.6Enrico Tassi
2017-06-07Merge pull request #129 from maximedenes/ssr-mergeMaxime Dénès
2017-06-07Change failing test.Maxime Dénès
2017-06-07For trunk, use merged ssr plugin.Maxime Dénès
2017-06-06Merge pull request #128 from maximedenes/remove-sigmaMaxime 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-06-05Merge pull request #123 from herbelin/trunk+pr590-patvarMaxime 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-28Merge pull request #126 from ejgallego/coqlib-part-02Maxime Dénès
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-25Merge pull request #124 from ejgallego/located_switchMaxime 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-17Merge pull request #120 from SkySkimmer/remove-vernacerrorEnrico
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-07Merge pull request #113 from ejgallego/no_camlp4_compatMaxime 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-04Merge pull request #1 from ppedrot/econstrMaxime Dénès
2017-04-04Fix ML compilation after introduction of EInstance.Pierre-Marie Pédrot
2017-04-03Merge pull request #118 from maximedenes/coq-pr417-landingEnrico
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-23ssrtest/elim.v: don't depend on FunctionEnrico Tassi
2017-03-21Merge pull request #108 from ejgallego/pp_new_fixMaxime Dénès
2017-03-21Merge pull request #111 from ejgallego/safe_stringEnrico
2017-03-17Merge pull request #117 from strub/ignore-ssrmatchingEnrico
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 14:18:31 +0000