aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
* Unify location handling of error functions.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
* | | Print the type-in-type flag in various user-facing functions.Gravatar Pierre-Marie Pédrot2016-06-18
|/ /
| * A hack to fix another regression with Ltac trace report in 8.5. E.g.Gravatar Hugo Herbelin2016-06-18
* | Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
* | Protect the beautifier from change in the lexer state (typically byGravatar Hugo Herbelin2016-06-16
* | Merge '/pr/206' into trunkGravatar Enrico Tassi2016-06-16
|\ \
* \ \ Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \ \
* | | | --print-version produces machine readable version infoGravatar Enrico Tassi2016-06-16
* | | | Merge remote-tracking branch 'github/pr/194' into trunkGravatar Maxime Dénès2016-06-16
|\ \ \ \
| | * | | Remove the syntax changes introduced by this branch.Gravatar Pierre-Marie Pédrot2016-06-15
| | * | | Allow `Pretyping.search_guard` to not check guardGravatar Arnaud Spiwack2016-06-15
| | * | | Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | | | | Preventive compatibility fixes for flushing.Gravatar Emilio Jesus Gallego Arias2016-06-14
* | | | | Fix for bug #4784Gravatar Emilio Jesus Gallego Arias2016-06-14
| | | * | Allow catching of EvaluatedError exceptions.Gravatar Emilio Jesus Gallego Arias2016-06-14
| |_|/ / |/| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 05:12:19 +0000