aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
* Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-08-17
|\
* | CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-11
| * Make it a bit more obvious when variables are of type unit.Gravatar Guillaume Melquiond2016-08-10
| * Reduce warning noise when compiling the standard library.Gravatar Guillaume Melquiond2016-08-09
|/
* Fix bug #4923: Warning: appcontext is deprecated.Gravatar Pierre-Marie Pédrot2016-07-18
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-13
|\
* \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\ \
| | * improved complexity in nsatzGravatar thery2016-07-06
| | * Bug Fixes : 4851 4858 4880 for nsatzGravatar thery2016-07-06
| |/
* | Revert "Merge remote-tracking branch 'github/pr/229' into trunk"Gravatar Maxime Dénès2016-07-05
| * Bug fix : variable capture in ltac code of NsatzGravatar thery2016-07-05
* | Merge remote-tracking branch 'github/pr/229' into trunkGravatar Maxime Dénès2016-07-04
|\ \
| | * congruence: Restrict refreshing to SetGravatar Matthieu Sozeau2016-07-04
| | * congruence: remove casts of indexed termsGravatar Matthieu Sozeau2016-07-04
| | * congruence/univs: properly refresh (fix #4609)Gravatar Matthieu Sozeau2016-07-04
* | | rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Gravatar Pierre Letouzey2016-07-03
* | | closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* | | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | | Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
* | | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
| * | Makefile: no bytecode compilation in make world, see make byte insteadGravatar Pierre Letouzey2016-06-29
|/ /
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\|
* | ssrmatching: avoid warnings about redundant typing clauses in ARGUMENT EXTENDGravatar Pierre Letouzey2016-06-27
* | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
* | Removing tactic compatibility layers in setoid_ring.Gravatar Pierre-Marie Pédrot2016-06-24
| * Fix typo.Gravatar Guillaume Melquiond2016-06-23
* | Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
* | Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* | Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* | Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
* | Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
* | Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-06-16
* | Adding printers for ring and field commands.Gravatar Hugo Herbelin2016-06-16
* | Fixing printing of Function.Gravatar Hugo Herbelin2016-06-16
* | Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \
* | | Remove inappropriate comment.Gravatar Maxime Dénès2016-06-16
| * | Remove the syntax changes introduced by this branch.Gravatar Pierre-Marie Pédrot2016-06-15
* | | ssrmatching: giving proper credits to the original author(s)Gravatar Enrico Tassi2016-06-15
* | | ssrmatching: ltac argument parsing made more robustGravatar Enrico Tassi2016-06-15
* | | ssrmatching: debug prints sent via msg_debugGravatar Enrico Tassi2016-06-15
* | | Rename "Set SsrMatchingDebug" into "Set Debug SsrMatching"Gravatar Enrico Tassi2016-06-15
| * | Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | | port ssrmatching plugin to the new makefileGravatar Enrico Tassi2016-06-14
* | | Merge remote-tracking branch 'origin/pr/146' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \
| | | * Merge branch 'bug4725' into v8.5Gravatar Matthieu Sozeau2016-06-14
| | | |\
* | | | \ Merge remote-tracking branch 'origin/pr/173' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 19:37:40 +0000