aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Add -compat 8.4 econstructor tactics, and testsGravatar Jason Gross2016-04-05
* Fix bug #4656Gravatar Jason Gross2016-04-05
* Update Coq84.vGravatar Jason Gross2016-04-04
* Add compatibility Nonrecursive Elimination SchemesGravatar Jason Gross2016-04-04
* Fixing the "No applicable tactic" non informative error messageGravatar Hugo Herbelin2016-04-03
* Update version number for 8.5pl1Gravatar Maxime Dénès2016-03-29
* Univs: fix get_current_context (bug #4603, part I)Gravatar Matthieu Sozeau2016-03-25
* Fix a bug in Program coercion codeGravatar Matthieu Sozeau2016-03-25
* Fix handling of arity of definitional classes.Gravatar Matthieu Sozeau2016-03-24
* use printf instead of sequenced calls to print.Gravatar Gregory Malecha2016-03-24
* add a .merlin target to the makefileGravatar Gregory Malecha2016-03-24
* Revert "refine: do check all unif problems are solved (Close: #4415, #4532)"Gravatar Enrico Tassi2016-03-23
* refine: do check all unif problems are solved (Close: #4415, #4532)Gravatar Enrico Tassi2016-03-23
* A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2016-03-22
* Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2016-03-22
* Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.Gravatar Pierre-Marie Pédrot2016-03-20
* Fix bug #4627: records with no declared arity can be template polymorphic.Gravatar Matthieu Sozeau2016-03-17
* Test file for #4623.Gravatar Maxime Dénès2016-03-17
* Fix #4623: set tactic too weak with universes (regression)Gravatar Maxime Dénès2016-03-17
* Test file for #4624, fixed by Matthieu's bfce815bd1.Gravatar Maxime Dénès2016-03-16
* Fix incorrect behavior of CS resolutionGravatar Matthieu Sozeau2016-03-16
* Fix #4591: Uncaught exception in directory browsing.Gravatar Pierre-Marie Pédrot2016-03-15
* CoqIDE is more resilient to initialization errors.Gravatar Pierre-Marie Pédrot2016-03-15
* Tentative fix for bug #4614: "Fully check the document" is uninterruptable.Gravatar Pierre-Marie Pédrot2016-03-15
* Try eta-expansion of records only on non-recursive onesGravatar Matthieu Sozeau2016-03-15
* Fix bug when a sort is ascribed to a RecordGravatar Matthieu Sozeau2016-03-15
* Trying to circumvent hdiutil error 5341 by padding.Gravatar Maxime Dénès2016-03-14
* According to Bruno, my fix for #4588 seems to be enough.Gravatar Maxime Dénès2016-03-11
* Primitive projections: protect kernel from erroneous definitions.Gravatar Matthieu Sozeau2016-03-10
* Hashconsing modules.Gravatar Pierre-Marie Pédrot2016-03-10
* Fix test-suite file coq-prog-argsGravatar Matthieu Sozeau2016-03-09
* Fixed bug #4533 with previous Keyed Unification commitGravatar Matthieu Sozeau2016-03-09
* Win: kill unreliable hence do not waitpid after kill -9 (Close #4369)Gravatar Enrico Tassi2016-03-09
* Fix strategy of Keyed UnificationGravatar Matthieu Sozeau2016-03-09
* Adding backtraces to scheme error messages.Gravatar Pierre-Marie Pédrot2016-03-07
* Re-enable OCaml warnings disabled by mistake as part of e759333.Gravatar Maxime Dénès2016-03-07
* Fixing bug #4608: Anomaly "output_value: abstract value (outside heap)".Gravatar Pierre-Marie Pédrot2016-03-05
* Fix #4607: do not read native code files if native compiler was disabled.Gravatar Maxime Dénès2016-03-04
* This fix is probably not enough to justify that there are no problems withGravatar Maxime Dénès2016-03-04
* Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
* Fix a typo in dev/doc/changes.txtGravatar Jason Gross2016-03-04
* Adding a test for the behaviour of open_constr described in #3777.Gravatar Pierre-Marie Pédrot2016-03-03
* Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.Gravatar Pierre-Marie Pédrot2016-03-03
* Fixing bug #4596: [rewrite] broke in the past few weeks.Gravatar Pierre-Marie Pédrot2016-02-28
* Document Hint Mode, cleanup Hint doc.Gravatar Matthieu Sozeau2016-02-24
* Document differences of Hint Resolve and Hint ExternGravatar Matthieu Sozeau2016-02-23
* Fix part of bug #4533: respect declared global transparency ofGravatar Matthieu Sozeau2016-02-23
* Fix bug #4544: Backtrack on using full betaiota reduction during keyed unific...Gravatar Matthieu Sozeau2016-02-23
* Fixing bug #4540: CoqIDE bottom progress bar does not update.Gravatar Pierre-Marie Pédrot2016-02-20
* Fix regression from 8.4 in reflexivity/...Gravatar Matthieu Sozeau2016-02-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 11:15:03 +0000