aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2016-08-09Reduce warning noise when compiling the standard library.Guillaume Melquiond
2016-07-18Fix bug #4923: Warning: appcontext is deprecated.Pierre-Marie Pédrot
2016-07-13Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-06improved complexity in nsatzthery
2016-07-06Bug Fixes : 4851 4858 4880 for nsatzthery
2016-07-05Revert "Merge remote-tracking branch 'github/pr/229' into trunk"Maxime Dénès
2016-07-05Bug fix : variable capture in ltac code of Nsatzthery
2016-07-04Merge remote-tracking branch 'github/pr/229' into trunkMaxime Dénès
2016-07-04congruence: Restrict refreshing to SetMatthieu Sozeau
2016-07-04congruence: remove casts of indexed termsMatthieu Sozeau
2016-07-04congruence/univs: properly refresh (fix #4609)Matthieu Sozeau
2016-07-03rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Pierre Letouzey
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Add and document match, fix and cofix reduction flags.Maxime Dénès
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-29Makefile: no bytecode compilation in make world, see make byte insteadPierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-27Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-27ssrmatching: avoid warnings about redundant typing clauses in ARGUMENT EXTENDPierre Letouzey
2016-06-27Adding ability to put any pattern in binders, prefixed by a quote.Daniel de Rauglaudre
2016-06-24Removing tactic compatibility layers in setoid_ring.Pierre-Marie Pédrot
2016-06-23Fix typo.Guillaume Melquiond
2016-06-18Reuse the typing_flags datatype for inductives.Pierre-Marie Pédrot
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-06-18Adding eintros to respect the e- prefix policy.Hugo Herbelin
2016-06-16Factorizing the uses of Declareops.safe_flags.Pierre-Marie Pédrot
2016-06-16Fixing a mispelling coma -> comma.Hugo Herbelin
2016-06-16Adding printers for ring and field commands.Hugo Herbelin
2016-06-16Fixing printing of Function.Hugo Herbelin
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-16Remove inappropriate comment.Maxime Dénès
2016-06-15Remove the syntax changes introduced by this branch.Pierre-Marie Pédrot
2016-06-15ssrmatching: giving proper credits to the original author(s)Enrico Tassi
2016-06-15ssrmatching: ltac argument parsing made more robustEnrico Tassi
2016-06-15ssrmatching: debug prints sent via msg_debugEnrico Tassi
2016-06-15Rename "Set SsrMatchingDebug" into "Set Debug SsrMatching"Enrico Tassi
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2016-06-14port ssrmatching plugin to the new makefileEnrico Tassi
2016-06-14Merge remote-tracking branch 'origin/pr/146' into trunkEnrico Tassi
2016-06-14Merge branch 'bug4725' into v8.5Matthieu Sozeau
2016-06-14Merge remote-tracking branch 'origin/pr/173' into trunkEnrico Tassi
2016-06-14Merge remote-tracking branch 'github/evarunsafe' into trunkMatthieu Sozeau
2016-06-09newring: fix for hack using evars as integers.Matthieu Sozeau
2016-06-08Compilation via pack for plugins of the stdlibPierre Letouzey
2016-06-08Officially discontinue the experimental coq build via ocamlbuildPierre Letouzey
2016-06-06STM: proof block detection/error resilience APIEnrico Tassi
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:10:36 +0000