aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-11-06Hugo's commentsMatthieu Sozeau
2016-11-06Maxime's commentsMatthieu Sozeau
2016-11-06Fixes from Enrico's reviewMatthieu Sozeau
2016-11-05Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr/gitroot/coq/coq into trunkMatej Kosik
2016-11-05FIX: dev/includeMatej Kosik
2016-11-05Not using style tags when translating/beautifying a file.Hugo Herbelin
2016-11-05Removing a special treatment for empty lines in comments.Hugo Herbelin
2016-11-05Removing obsolete parsing of strings à la v7 in comments.Hugo Herbelin
2016-11-05Credits for 8.6Matthieu Sozeau
2016-11-05Minor fix in documentationMatthieu Sozeau
2016-11-05Do not print dependent evars by default (expensive)Matthieu Sozeau
2016-11-05More precise refine compatibilityMatthieu Sozeau
2016-11-04Quick fix of tactic parsing while Load-ing in coqide.Hugo Herbelin
2016-11-04Test for #4966 ("auto" wrongly seen as "auto with *" when in position of ident).Hugo Herbelin
2016-11-04Fix #3441 Use pf_get_type_of to avoid blowupMatthieu Sozeau
2016-11-04Fix refine in compatibility modeMatthieu Sozeau
2016-11-04Fix #4837: ./configure -local makes coqdep issue many warningsMaxime Dénès
2016-11-04Merge remote-tracking branch 'github/pr/335' into v8.6Maxime Dénès
2016-11-04Merge remote-tracking branch 'github/pr/336' into v8.6Maxime Dénès
2016-11-04Add documentation for [Set Warnings] and the -w option.Cyprien Mangin
2016-11-04Silence option deprecation warnings in the compat fileJason Gross
2016-11-03Remove an OCaml 4.02 construct.Maxime Dénès
2016-11-03Merge remote-tracking branch 'github/pr/340' into v8.6Maxime Dénès
2016-11-03Rework search_strategy option handlingMatthieu Sozeau
2016-11-03Internal API change to typeclasses eauto.Théo Zimmermann
2016-11-03Do not shelve non-class subgoals but fail, it shouldMatthieu Sozeau
2016-11-03Fix test-suite files relying on tcs bugsMatthieu Sozeau
2016-11-03Fixed bug #4095.Matthieu Sozeau
2016-11-03typeclasses eauto Implem/doc of shelving strategyMatthieu Sozeau
2016-11-03Fix [typeclasses eauto with] and nopattern hintsMatthieu Sozeau
2016-11-03Fix handling of only_classes at toplevelMatthieu Sozeau
2016-11-03Test new syntax for hints and typeclass optionsMatthieu Sozeau
2016-11-03Handle Unique Solutions flag.Matthieu Sozeau
2016-11-03TCS: error handling and debug printing in resolutionMatthieu Sozeau
2016-11-03Fix bugs in Filtered Unification and cleanup codeMatthieu Sozeau
2016-11-03Fix Typeclasses eauto := bfs.Matthieu Sozeau
2016-11-03Lets Hints/Instances take an optional patternMatthieu Sozeau
2016-11-03Document options of typeclasses (eauto)Matthieu Sozeau
2016-11-03Revert "Better Arguments compatibility."Maxime Dénès
2016-11-03Merge branch 'v8.6' into trunkMaxime Dénès
2016-11-03Merge remote-tracking branch 'github/pr/341' into v8.6Maxime Dénès
2016-11-03updating ".merlin" fileMatej Kosik
2016-11-02Better Arguments compatibility.Maxime Dénès
2016-11-02Fix various shortcomings of the warnings infrastructure.Maxime Dénès
2016-11-02Put string between quotes when printing an option value.Maxime Dénès
2016-10-31Moving unused code out of the kernel into Termops.Pierre-Marie Pédrot
2016-10-31Stronger static invariant in equality upto universes.Pierre-Marie Pédrot
2016-10-31Code factorization in Universes.Pierre-Marie Pédrot
2016-10-30Moving Universes to the engine/ folder.Pierre-Marie Pédrot
2016-10-30Reordering Termops w.r.t. Evd and Namegen in engine folder.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-18 02:53:45 +0000