aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Allowing to extend the Print Grammar command generically.Gravatar Pierre-Marie Pédrot2016-09-14
* Making Proof_global terminator generic in external tactics.Gravatar Pierre-Marie Pédrot2016-09-08
* Unplugging Tacexpr in several interface files.Gravatar Pierre-Marie Pédrot2016-09-08
* Making Vernacexpr independent from Tacexpr.Gravatar Pierre-Marie Pédrot2016-09-08
* Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\
* \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\ \
| * | Fix #4941 - ~/.coqrc file confusing locationsGravatar Maxime Dénès2016-08-30
* | | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30
* | | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30
* | | CLEANUP: taking advantage of "_ % _" operator to express function composition...Gravatar Matej Kosik2016-08-29
| * | Support qualified identifiers in Show Match (bug #5050).Gravatar Guillaume Melquiond2016-08-27
* | | Merge remote-tracking branch 'v8.6' into trunkGravatar Matej Kosik2016-08-25
|\| |
| * | Do not export an internal function in Namegen.Gravatar Pierre-Marie Pédrot2016-08-25
* | | CLEANUP: removing calls of the "Context.Named.Declaration.get_value" functionGravatar Matej Kosik2016-08-25
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| * | 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
| |_|/ / |/| | |
| | | * 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
| |_|/ |/| |
| | * [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