aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-06-27Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails ↵Maxime Dénès
with make -j4
2017-06-27Merge PR#731: Mini-cleaning around OCaml file namesMaxime Dénès
This is only a partial merge, we stick with using the standard OCaml (un)capitalize functions.
2017-06-27A cleaning phase about ocaml file names.Hugo Herbelin
Ocaml file names are restricted since 2008 to A..Z followed by a..z0..9'_. We take this constraint into account in tools manipulating Ocaml file names.
2017-06-27Preparing to hints supporting discharge.Hugo Herbelin
I.e., do not set local flag to false when in a section since compatibility tells discharge of hints is not supported.
2017-06-27Merge PR#814: Fix #5380: Default colors for CoqIDE are actually applied.Maxime Dénès
2017-06-26Merge PR#826: Put plugin exports in the right compatibility fileMaxime Dénès
2017-06-26disable async on Windows by defaultPaul Steckler
2017-06-26Merge PR#825: Ignore all PDF files.Maxime Dénès
2017-06-26Merge PR#828: closing bug #4250Maxime Dénès
2017-06-26Bump version number to 8.6.1.Maxime Dénès
2017-06-26Fix libpcre dependency issue under Windows.Maxime Dénès
2017-06-26Fix proxy setting issueMichael Soegtrop
2017-06-26Fixes bug #5561,#5562 in Windows build systemMichael Soegtrop
2017-06-26Merge PR#756: Fix Bug #5574, document function scopeMaxime Dénès
2017-06-25Reorganizing functions to find the relative position of an hypothesis.Hugo Herbelin
Also fixing a bug of get_next_hyp_position when the hypothesis is the oldest of the context (see test in ltac.v).
2017-06-25Moving "assert" (internally "Cut") to the new proof engine.Hugo Herbelin
It allows in particular to have "Info" on tactic "assert" and derivatives not to give an "<unknown>".
2017-06-25Exporting general-purpose functions on goal contexts from "logic.ml" to ↵Hugo Herbelin
"tactics.ml". This is in preparation of move of "assert" from old to new proof engine.
2017-06-25Adding intermediate entry point to create an evar in empty rel_context.Hugo Herbelin
2017-06-23Merge PR#824: Fix printersMaxime Dénès
2017-06-23Merge PR#821: [vernac] Remove stale bool parameter from ↵Maxime Dénès
`VernacStartTheoremProof`
2017-06-23Merge PR#820: [ide] Correct more merging errors.Maxime Dénès
2017-06-23Merge PR#815: STM: par: report no error to UIs in non-solve modeMaxime Dénès
2017-06-23Merge PR#794: Cleanup of ltac cmxsMaxime Dénès
2017-06-23Merge PR#762: [vernac] Fix unneeded mutual references in ObligationsMaxime Dénès
2017-06-23Merge PR#813: Fix plugin warningsMaxime Dénès
2017-06-23Fix Bug #5574, document function scopePaul Steckler
2017-06-23closing bug #4250Julien Forest
2017-06-23[configure] 'ocaml' is more precise than OCaml as we mean the binary.Maxime Dénès
Fix suggested by Hugo.
2017-06-23ocaml -> OCaml in configure.ml.Maxime Dénès
2017-06-23Merge PR#729: Fixing an inconsistency between configure and configure.mlMaxime Dénès
2017-06-23Merge PR#740: Refactor documentation of records.Maxime Dénès
2017-06-23Add tests for handling of warningsTej Chajed
2017-06-23Fix bug 5392: Warnings defined in plugins are considered unknownMaxime Dénès
The status of a warning can now be set before the warning is declared (typically by a plugin). However, I had to remove the "unknown warning" warning.
2017-06-23In enter_one, not having exactly one goal is a fatal error of the monad.Hugo Herbelin
Pointed out by PMP.
2017-06-22Add test-suite file for funind, extraction with compat 8.6Jason Gross
2017-06-22Put plugin exports in the right compatibility fileJason Gross
This closes [bug #5607](https://coq.inria.fr/bugs/show_bug.cgi?id=5607). PR #220 put the exports in the wrong compat files, presumably because it was originally targeted to version 8.6, and this wasn't updated when it was retargeted to version 8.7.
2017-06-22Ignore all PDF files.Théo Zimmermann
Rules for ignoring *some* PDF files had been added one by one to `.gitignore` but some were still missing (for the corresponding latex files in `dev`). This rule is actually better since we are not tracking any PDF file.
2017-06-22Merge PR#817: [stm] Fix route setting on VtQueryMaxime Dénès
2017-06-22Add missing definition and fix #use include;; as suggested by @amintimany.Théo Zimmermann
2017-06-21[vernac] Remove stale bool parameter from `VernacStartTheoremProof`Emilio Jesus Gallego Arias
`VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today.
2017-06-21[ide] Correct more merging errors.Emilio Jesus Gallego Arias
This file doesn't want to leave us.
2017-06-21Should fix a false negative reported by deps-order.sh.Hugo Herbelin
The files deps-order.sh and deps-checksum.sh were concurrently rm-ing the files of the other. Courtesy of Guillaume M.
2017-06-20[stm] Fix route setting on VtQueryEmilio Jesus Gallego Arias
This is a fix for a mistake in d8874dd855d748aaaf504890487ab15ffd7a677d , where we forgot to propagate the route parameter.
2017-06-20STM: par: report no error to UIs in non-solve modeEnrico Tassi
Used to report to the UI an Error feedback message whenever a worker was non making any progress. This is wrong since no-progress is fine (as long as one does not specify "solve")
2017-06-20Default colors for CoqIDE are actually applied.Cyprien Mangin
This fixes bug #5380 in particular. More generally, tags were not updated to the correct default value if the corresponding line in the configuration file was missing.
2017-06-20Remove dead code [Universes.simplify_universe_context]Gaëtan Gilbert
Dead since 23f4804b50307766219392229757e75da9aa41d9
2017-06-20[vernac] Remove forward hooks from Obligations.Emilio Jesus Gallego Arias
This was (once again) a spurious inter-dependency, that we solve by introducing a new module with the proper functionality. This helps in cleaning up the code. Note that no code was changed, other than removing the setting of the references.
2017-06-20[vernac] Remove unused hooks.Emilio Jesus Gallego Arias
These hooks are not used (leftovers?) and IMHO they should not be.
2017-06-20Merge PR#812: Use more neutral wording instead of mentioning CoqIDEMaxime Dénès
2017-06-20Merge PR#742: Fix `make TIMED=1` garbageMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-27 08:08:30 +0000