aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-04-04Add compatibility Nonrecursive Elimination SchemesJason Gross
2016-04-03Fixing the "No applicable tactic" non informative error messageHugo Herbelin
2016-03-29Update version number for 8.5pl1Maxime Dénès
2016-03-25Univs: fix get_current_context (bug #4603, part I)Matthieu Sozeau
2016-03-25Fix a bug in Program coercion codeMatthieu Sozeau
2016-03-24Fix handling of arity of definitional classes.Matthieu Sozeau
2016-03-24use printf instead of sequenced calls to print.Gregory Malecha
2016-03-24add a .merlin target to the makefileGregory Malecha
2016-03-23Revert "refine: do check all unif problems are solved (Close: #4415, #4532)"Enrico Tassi
2016-03-23refine: do check all unif problems are solved (Close: #4415, #4532)Enrico Tassi
2016-03-22A patch renaming equal into eq in the module dealing withHugo Herbelin
2016-03-22Adding eq/compare/hash for syntactic view atHugo Herbelin
2016-03-20Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.Pierre-Marie Pédrot
2016-03-17Fix bug #4627: records with no declared arity can be template polymorphic.Matthieu Sozeau
2016-03-17Test file for #4623.Maxime Dénès
2016-03-17Fix #4623: set tactic too weak with universes (regression)Maxime Dénès
2016-03-16Test file for #4624, fixed by Matthieu's bfce815bd1.Maxime Dénès
2016-03-16Fix incorrect behavior of CS resolutionMatthieu Sozeau
2016-03-15Fix #4591: Uncaught exception in directory browsing.Pierre-Marie Pédrot
2016-03-15CoqIDE is more resilient to initialization errors.Pierre-Marie Pédrot
2016-03-15Tentative fix for bug #4614: "Fully check the document" is uninterruptable.Pierre-Marie Pédrot
2016-03-15Try eta-expansion of records only on non-recursive onesMatthieu Sozeau
2016-03-15Fix bug when a sort is ascribed to a RecordMatthieu Sozeau
2016-03-14Trying to circumvent hdiutil error 5341 by padding.Maxime Dénès
2016-03-11According to Bruno, my fix for #4588 seems to be enough.Maxime Dénès
2016-03-10Primitive projections: protect kernel from erroneous definitions.Matthieu Sozeau
2016-03-10Hashconsing modules.Pierre-Marie Pédrot
2016-03-09Fix test-suite file coq-prog-argsMatthieu Sozeau
2016-03-09Fixed bug #4533 with previous Keyed Unification commitMatthieu Sozeau
2016-03-09Win: kill unreliable hence do not waitpid after kill -9 (Close #4369)Enrico Tassi
2016-03-09Fix strategy of Keyed UnificationMatthieu Sozeau
2016-03-07Adding backtraces to scheme error messages.Pierre-Marie Pédrot
2016-03-07Re-enable OCaml warnings disabled by mistake as part of e759333.Maxime Dénès
2016-03-05Fixing bug #4608: Anomaly "output_value: abstract value (outside heap)".Pierre-Marie Pédrot
2016-03-04Fix #4607: do not read native code files if native compiler was disabled.Maxime Dénès
2016-03-04This fix is probably not enough to justify that there are no problems withMaxime Dénès
2016-03-04Rename Ephemeron -> CEphemeron.Maxime Dénès
2016-03-04Fix a typo in dev/doc/changes.txtJason Gross
2016-03-03Adding a test for the behaviour of open_constr described in #3777.Pierre-Marie Pédrot
2016-03-03Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.Pierre-Marie Pédrot
2016-02-28Fixing bug #4596: [rewrite] broke in the past few weeks.Pierre-Marie Pédrot
2016-02-24Document Hint Mode, cleanup Hint doc.Matthieu Sozeau
2016-02-23Document differences of Hint Resolve and Hint ExternMatthieu Sozeau
2016-02-23Fix part of bug #4533: respect declared global transparency ofMatthieu Sozeau
2016-02-23Fix bug #4544: Backtrack on using full betaiota reduction during keyed unific...Matthieu Sozeau
2016-02-20Fixing bug #4540: CoqIDE bottom progress bar does not update.Pierre-Marie Pédrot
2016-02-19Fix regression from 8.4 in reflexivity/...Matthieu Sozeau
2016-02-19Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance.Pierre-Marie Pédrot
2016-02-19Fixing bug #4582: cannot override notation [ x ].Pierre-Marie Pédrot
2016-02-19STM: Print/Extraction have to be skipped if -quickEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 01:51:57 +0000