aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-11-08Adding a debugging printer for ident maps whose codomain type is unknown.Hugo Herbelin
Actually, ocaml is apparently doing well. If there is a printer for 'a Id.Map.t and another for say Id.t Id.Map.id, it uses the most defined existing ones, so, it is apparently not a problem to have overlapping printer.
2017-11-08Remove dependency of test-suite on git (fix #5725).Théo Zimmermann
The two lines that this commit remove are spurious as a `git clean -dfx || true` is already performed in `test-suite/coq-makefile/template/init.sh`. While this resolves the accidental dependency on git, I am still unhappy with this call of `git clean -dfx`.
2017-11-08Merge PR #6100: [api] Remove 8.7 ML-deprecated functions.Maxime Dénès
2017-11-08Merge PR #6096: Documentation: "tac1 || tac2" means "first [ progress tac1 | ↵Maxime Dénès
tac2 ]"
2017-11-08Merge PR #6087: [feedback] Helper to print feedback messages in the console.Maxime Dénès
2017-11-08Merge PR #6086: [ci] Switch VST back to upstream.Maxime Dénès
2017-11-08Merge PR #922: New beta-iota compatibility refinementsMaxime Dénès
2017-11-08Fixing missing separator in an error message.Hugo Herbelin
The message is the "Conversion test raised an anomaly" one.
2017-11-08Fixing an (apparently misplaced) spc in anomaly reporting message.Hugo Herbelin
2017-11-07Hack to restore printing of glob_constr in debugger.Hugo Herbelin
2017-11-07[api] Remove 8.7 ML-deprecated functions.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
We do up to `Term` which is the main bulk of the changes.
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
This will allow to merge back `Names` with `API.Names`
2017-11-06Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.Maxime Dénès
2017-11-06Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]",Samuel Gruetter
not "first [ progress tac1 | progress tac2 ]". And add a missing backslash.
2017-11-06Generalize the use of repr in Tac2stdlib.Pierre-Marie Pédrot
2017-11-06Remove packaging scripts while waiting for a fix to #5998.Théo Zimmermann
This is a temporary commit which should be reverted once the issue is fixed.
2017-11-06[feedback] Helper to print feedback messages in the console.Emilio Jesus Gallego Arias
This is useful for tools such as `coqchk` or `coq_makefile` that want to handle feedback on their own.
2017-11-06Merge PR #6072: Protecting evar map printerMaxime Dénès
2017-11-06Merge PR #6074: Refining PR#924 (insensitivity of projection heuristics to ↵Maxime Dénès
alphabet).
2017-11-06Merge PR #6085: Update .mailmap with a jkloos aliasMaxime Dénès
2017-11-06Merge PR #6063: Finish removing Show Goal uidMaxime Dénès
2017-11-06Merge PR #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" ↵Maxime Dénès
rules
2017-11-06Merge PR #1139: Add a linter.Maxime Dénès
2017-11-05Update .mailmap with a jkloos aliasJason Gross
2017-11-05Refining PR#924 (insensitivity of projection heuristics to alphabet).Hugo Herbelin
We refine the criterion for selecting a projection. Before PR#924 it was alphabetic (i.e. morally "random" up to alpha-conversion). After PR#924 it was chronological. We refine a bit more by giving priority to simple projections when they exist over projections which include an evar instantiation (and which may actually be ill-typed).
2017-11-05Cosmetic changes in evar_map printer.Hugo Herbelin
2017-11-05Preventively protect locally against failures of evar_map printer.Hugo Herbelin
It is not clear that this is really needed, but in case it happens, one will at least have a partial result available rather than an unexploitable global failure of the parser.
2017-11-05Fixing a cause of failure of evar_map printer in debugger.Hugo Herbelin
Indeed, the debugger debugs coqtop but it is itself just an ocaml runtime extended with the coq printers. It does not know the environment, so, looking in the Global.env() for the printers can only fail.
2017-11-04[ci] Add Ltac2Jason Gross
2017-11-04A possible fix after PR#6047 (a generic printer for ltac values).Hugo Herbelin
2017-11-04[api] Deprecate all legacy uses of Name.Id in core.Emilio Jesus Gallego Arias
This is a first step towards some of the solutions proposed in #6008.
2017-11-04Finish removing Show Goal uidGaëtan Gilbert
Syntax removed in faa064c746e20a12b3c8f792f69537b18e387be6
2017-11-04Adding support for syntax "let _ := e in e'" in Ltac.Hugo Herbelin
Adding a file fixing #5996 and which uses this feature.
2017-11-03Merge PR #6060: Improve error message and fix #6055 (spelling mistake).Maxime Dénès
2017-11-03Merge PR #6051: Fix FIXME: use OCaml 4.02 generative functors when available.Maxime Dénès
2017-11-03Merge PR #6047: A generic printer for ltac valuesMaxime Dénès
2017-11-03Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous ↵Maxime Dénès
variables).
2017-11-03Merge PR #6036: [toplevel] Export the last document seen after `Drop`.Maxime Dénès
2017-11-03Merge PR #6031: [ci] Switch back to upstream version of Math-Classes and Corn.Maxime Dénès
2017-11-03Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in ↵Maxime Dénès
dev/doc/changes.
2017-11-03Merge PR #6024: Update of Coq version historyMaxime Dénès
2017-11-03Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).Maxime Dénès
2017-11-03Merge PR #5999: An attempt to fix issue #5771 (error color hidden by warning ↵Maxime Dénès
color in coqide).
2017-11-03Merge PR #924: Fixing part of #5669: unification heuristics sensitive to ↵Maxime Dénès
alphabet
2017-11-02Update tactics.mlFarzon Lotfi
fix spelling mistake. reword message to be in the Present Perfect tense instead of the 3rd person present because action is completed with respect to the theorem not some unknown third person.
2017-11-02Fix the horrible syntax that used to be valid for tuple matching.Pierre-Marie Pédrot
2017-11-02Factorizing entries for patterns with type constraints.Pierre-Marie Pédrot
2017-11-02Remove redundant env argument to Reduction.ccnvGaëtan Gilbert
The infos already contain the env. Note that it was only actually used in the 2 lookup_mind lines.
2017-11-02Moving pattern type constraints to pattern AST.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-19 05:51:04 +0000