aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* | FIX: HTML version of Chapter 4 of the Reference ManualGravatar Matej Kosik2016-04-12
* | TYPOGRAPHY: adding missing \noindent macrosGravatar Matej Kosik2016-04-12
* | Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.vGravatar Nickolai Zeldovich2016-04-09
* | Added compatibility coercions from Specif.v which were present in Coq 8.4.Gravatar Hugo Herbelin2016-04-08
* | Fixing a source of inefficiency and an artificial dependency in theGravatar Daniel de Rauglaudre2016-04-08
* | Allow to unset the refinement mode of Instance in MLGravatar Matthieu Sozeau2016-04-07
* | Fixing an incorrect use of prod_appvect on a term which was not aGravatar Hugo Herbelin2016-04-07
* | Merge PR#152: Add -compat 8.4 econstructor tactics, and testsGravatar Maxime Dénès2016-04-07
|\ \
* | | Use -win32 and -win64 suffixes for installer name on Windows.Gravatar Maxime Dénès2016-04-07
| * | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 02:45:12 +0000