aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2016-09-29Fix bug #4798: compat notations should not modify the parser.Pierre-Marie Pédrot
2016-09-29Arguments: cleanup + detect discrepancy rename/implicit (#3753)Enrico Tassi
2016-09-29Merge branch 'bug4723' into v8.6Matthieu Sozeau
2016-09-29fix bug 3683 : adds references to the web site for the bug trackerYves Bertot
2016-09-29Fix bug #5011: Anomaly on [Existing Class].Pierre-Marie Pédrot
2016-09-29Cleanup API, making inference_hook optionalMatthieu Sozeau
2016-09-29Argument : assert does fail if no arg is given (fix #4864)Enrico Tassi
2016-09-29-profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100)Enrico Tassi
2016-09-28Fix bug #4723 and FIXME in API for solve_by_tacMatthieu Sozeau
2016-09-25The coqtop options -Q and -R do not affect the ML loadpath anymore.Pierre-Marie Pédrot
2016-09-22coqc -o now places .glob file near .vo fileEnrico Tassi
2016-09-19Fix warning when using Variables at toplevel.Maxime Dénès
2016-09-13coqc: print debug feedback coming from workersEnrico Tassi
2016-09-10Avoid putting a useless "toploop" directory in the ML search path if it does ...Guillaume Melquiond
2016-09-09Make it explicit when paths are added to the ML search paths.Guillaume Melquiond
2016-09-08Avoid canonizing the same paths over and over.Guillaume Melquiond
2016-08-30Fix #4941 - ~/.coqrc file confusing locationsMaxime Dénès
2016-08-27Support qualified identifiers in Show Match (bug #5050).Guillaume Melquiond
2016-08-25Do not export an internal function in Namegen.Pierre-Marie Pédrot
2016-08-24Properly compute types for assumed section variables (bug #5035).Guillaume Melquiond
2016-08-24Merge PR #260: "Fix bug 4842 (Time prints in multiple lines)" into v8.6Pierre-Marie Pédrot
2016-08-24Merge PR #258: "Fix newline issues" into v8.6Pierre-Marie Pédrot
2016-08-23Arguments: give / after last ! error detection fixedEnrico Tassi
2016-08-23fix get_host_port error message (#4724)Enrico Tassi
2016-08-21Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-08-20Fixing an anomaly in printing a unification error message.Hugo Herbelin
2016-08-19[pp] Fix bug 4842 (Time prints in multiple lines)Emilio Jesus Gallego Arias
2016-08-19[pp] Fix newline issues.Emilio Jesus Gallego Arias
2016-08-16Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-08-11Do not assume the "TERM" environment variable is always set (bug #5007).Guillaume Melquiond
2016-07-29Merge remote-tracking branch 'gforge/v8.5' into v8.6Matthieu Sozeau
2016-07-29Fix bug #3886, generation of obligations of fixesMatthieu Sozeau
2016-07-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-07Prevent "Load" from displaying all the intermediate subgoals.Guillaume Melquiond
2016-07-07Do not display goals in -compile-verbose mode (bug #4841).Guillaume Melquiond
2016-07-07Program: fix #4873: transparency option not usedMatthieu Sozeau
2016-07-06Renaming to more generic has_dependent_elim testMatthieu Sozeau
2016-07-06Move is_prim... to Inductiveops and correct SchemeMatthieu Sozeau
2016-07-06primproj: warning and avoid error.Matthieu Sozeau
2016-07-06Fix #4793: Coq 8.6 should accept -compat 8.6Maxime Dénès
2016-07-03rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Pierre Letouzey
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-29Univs: Fix bug #4726Matthieu Sozeau
2016-06-29Univs: earlier errors for strict univ decls #4527Matthieu Sozeau
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-28Properly handle the only printing flag in Reserved Notations.Pierre-Marie Pédrot
2016-06-28Properly handling the only printing flag when parsing rules already exist.Pierre-Marie Pédrot
2016-06-27Program: refine shrinking of obligationsMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-14 20:25:03 +0000