aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Fix warning when using Variables at toplevel.Gravatar Maxime Dénès2016-09-19
* coqc: print debug feedback coming from workersGravatar Enrico Tassi2016-09-13
* Avoid putting a useless "toploop" directory in the ML search path if it does ...Gravatar Guillaume Melquiond2016-09-10
* Make it explicit when paths are added to the ML search paths.Gravatar Guillaume Melquiond2016-09-09
* Avoid canonizing the same paths over and over.Gravatar Guillaume Melquiond2016-09-08
* Fix #4941 - ~/.coqrc file confusing locationsGravatar Maxime Dénès2016-08-30
* Support qualified identifiers in Show Match (bug #5050).Gravatar Guillaume Melquiond2016-08-27
* Do not export an internal function in Namegen.Gravatar Pierre-Marie Pédrot2016-08-25
* Properly compute types for assumed section variables (bug #5035).Gravatar Guillaume Melquiond2016-08-24
* Merge PR #260: "Fix bug 4842 (Time prints in multiple lines)" into v8.6Gravatar Pierre-Marie Pédrot2016-08-24
|\
* \ Merge PR #258: "Fix newline issues" into v8.6Gravatar Pierre-Marie Pédrot2016-08-24
|\ \
* | | Arguments: give / after last ! error detection fixedGravatar Enrico Tassi2016-08-23
* | | fix get_host_port error message (#4724)Gravatar Enrico Tassi2016-08-23
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-21
|\ \ \
| * | | Fixing an anomaly in printing a unification error message.Gravatar Hugo Herbelin2016-08-20
| | | * [pp] Fix bug 4842 (Time prints in multiple lines)Gravatar Emilio Jesus Gallego Arias2016-08-19
| |_|/ |/| |
| | * [pp] Fix newline issues.Gravatar Emilio Jesus Gallego Arias2016-08-19
| |/ |/|
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\|
| * Do not assume the "TERM" environment variable is always set (bug #5007).Gravatar Guillaume Melquiond2016-08-11
* | Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-29
|\|
| * Fix bug #3886, generation of obligations of fixesGravatar Matthieu Sozeau2016-07-29
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\|
| * Prevent "Load" from displaying all the intermediate subgoals.Gravatar Guillaume Melquiond2016-07-07
| * Do not display goals in -compile-verbose mode (bug #4841).Gravatar Guillaume Melquiond2016-07-07
* | Program: fix #4873: transparency option not usedGravatar Matthieu Sozeau2016-07-07
* | Renaming to more generic has_dependent_elim testGravatar Matthieu Sozeau2016-07-06
* | Move is_prim... to Inductiveops and correct SchemeGravatar Matthieu Sozeau2016-07-06
* | primproj: warning and avoid error.Gravatar Matthieu Sozeau2016-07-06
* | Fix #4793: Coq 8.6 should accept -compat 8.6Gravatar Maxime Dénès2016-07-06
* | 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
* | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* | Univs: Fix bug #4726Gravatar Matthieu Sozeau2016-06-29
* | Univs: earlier errors for strict univ decls #4527Gravatar Matthieu Sozeau2016-06-29
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* | Properly handle the only printing flag in Reserved Notations.Gravatar Pierre-Marie Pédrot2016-06-28
* | Properly handling the only printing flag when parsing rules already exist.Gravatar Pierre-Marie Pédrot2016-06-28
* | Program: refine shrinking of obligationsGravatar Matthieu Sozeau2016-06-27
* | Rework treatment of default transparency of obligationsGravatar Matthieu Sozeau2016-06-27
* | Shrink Proofs/Obligations by default and deprecateGravatar Matthieu Sozeau2016-06-27
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\|
* | Merge remote-tracking branch 'github/pr/223' into feedback-locationsGravatar Maxime Dénès2016-06-27
|\ \
* | | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| * | [feedback] Add optional ?loc parameter to loggers.Gravatar Emilio Jesus Gallego Arias2016-06-25
|/ /
* | Merge remote-tracking branch 'github/pr/212' into trunkGravatar Maxime Dénès2016-06-20
|\ \
| * | Add file name, line number and beginning of line position to locations.Gravatar Maxime Dénès2016-06-20
* | | Fix bug #4836: Anomaly: Uncaught exception Invalid_argument.Gravatar Pierre-Marie Pédrot2016-06-19
* | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-26 19:08:39 +0000