aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-12-21Do not exclude "opened" bugs from reportMaxime Dénès
2018-12-21Merge PR #9182: Stop printing Monomorphic/Polymorphic in Print.Maxime Dénès
2018-12-20Merge PR #8488: Warning when using automatic template polymorphismPierre-Marie Pédrot
2018-12-20Merge PR #9200: [ssr] make `>` stand aloneMaxime Dénès
2018-12-19Add CHANGES for auto-template warning.Gaëtan Gilbert
2018-12-19Put #[universes(template)] in outputs testsGaëtan Gilbert
2018-12-19Put #[universes(template)] on all auto template spots in stdlibGaëtan Gilbert
2018-12-19warn when using auto template, funind never uses template polyGaëtan Gilbert
The warning can be avoided with the attributes, (or just disable the warning itself I guess).
2018-12-19Merge PR #9139: [engine] Allow debug printers to access the environment.Pierre-Marie Pédrot
2018-12-19Merge PR #9159: Make ugraph implementation abstract wrt universe specificsPierre-Marie Pédrot
2018-12-19Merge PR #9231: Fixes #9229: Infix not robust wrt choice of variable names ↵Pierre-Marie Pédrot
in right-hand side
2018-12-19Merge PR #9237: Add Map.find_optPierre-Marie Pédrot
2018-12-19[doc] typoEnrico Tassi
2018-12-19Merge PR #9081: [dune] A new Makefile.dune target for each package (coq, ↵Théo Zimmermann
coqide-server and coqide).
2018-12-19[dune] Add targets for Coq individual packages.Emilio Jesus Gallego Arias
2018-12-18Merge PR #9223: Fix universe restriction in delayed mode.Pierre-Marie Pédrot
2018-12-18[ssr] make > a stand alone intro patternEnrico Tassi
2018-12-18Merge PR #6705: [ssr] extended intro patternsCyril Cohen
2018-12-18Fixes #9229 (Infix not robust wrt choice of variable names).Hugo Herbelin
2018-12-18[ssr] new test by Arthur CharguéraudEnrico Tassi
2018-12-18[ssr] extended intro patterns: + > [^] /ltac:Enrico Tassi
This commit implements the following intro patterns: Temporary "=> +" "move=> + stuff" ==== "move=> tmp stuff; move: tmp" It preserves the original name. "=>" can be chained to force generalization as in "move=> + y + => x z" Tactics as views "=> /ltac:(tactic)" Supports notations, eg "Notation foo := ltac:(bla bla bla). .. => /foo". Limited to views on the right of "=>", views that decorate a tactic as move or case are not supported to be tactics. Dependent "=> >H" move=> >H ===== move=> ???? H, with enough ? to name H the first non-dependent assumption (LHS of the first arrow). TC isntances are skipped. Block intro "=> [^ H] [^~ H]" after "case" or "elim" or "elim/v" it introduces in one go all new assumptions coming from the eliminations. The names are picked from the inductive type declaration or the elimination principle "v" in "elim/v" and are appended/prepended the seed "H" The implementation makes crucial use of the goal_with_state feature of the tactic monad. For example + schedules a generalization to be performed at the end of the intro pattern and [^ .. ] reads the name seeds from the state (that is filled in by case and elim).
2018-12-18[arguments] cleanupEnrico Tassi
2018-12-18Merge PR #9218: [STM] Better protection for cur_idEnrico Tassi
2018-12-18Merge PR #9222: Fix classification of Set Default Proof Mode.Enrico Tassi
2018-12-18Add comment to acyclicgraph APIGaëtan Gilbert
2018-12-18Merge PR #9160: Avoid user-given names in automatic introduction of bindersPierre-Marie Pédrot
2018-12-18Merge PR #9178: CoqIDE: Restoring configuration of default width/height of ↵Pierre-Marie Pédrot
main window.
2018-12-18Merge PR #9215: Set up CI with Azure PipelinesEmilio Jesus Gallego Arias
2018-12-17Merge PR #9153: [api] Move reduction modules to `tactics`Pierre-Marie Pédrot
2018-12-17[STM] Better protection for cur_idMaxime Dénès
Since some state handling refactoring, `purify_stm` was no longer protecting against assignement of cur_id, resulting in confusing behavior w.r.t. cache.
2018-12-17Merge PR #9238: CI: simple-io now depends on ext-libEmilio Jesus Gallego Arias
2018-12-17Set up CI with Azure PipelinesGaëtan Gilbert
2018-12-17simple-io now depends on ext-libGaëtan Gilbert
2018-12-17Merge PR #8856: [gitlab] Test Ocaml trunk.Gaëtan Gilbert
2018-12-17Restrict body universes in delayed mode.Gaëtan Gilbert
2018-12-17Fix git line ending conversion in windowsGaëtan Gilbert
2018-12-17Stop printing Monomorphic/Polymorphic in Print.Gaëtan Gilbert
You can tell which it is from the `@{}` if you really care, and seeing `Monomorphic List (A:Type)` with no indication that `Monomorphic` is about universes can confuse people.
2018-12-17Remove universe specific terminology from acyclicgraphGaëtan Gilbert
This means removing [univ], [level] and derived abbreviations like [lvl]. We keep using u, v for variable names as doing otherwise would be too intrusive, and it's not overly universe specific.
2018-12-17Make ugraph implementation abstract wrt universe specificsGaëtan Gilbert
This should give better visibility of universe specific operations vs generic graph operations.
2018-12-17Add Map.find_optGaëtan Gilbert
2018-12-17Fix classification of Set Default Proof Mode.Gaëtan Gilbert
2018-12-17Merge PR #9206: [stm] join the tip of the document even when fixing a proof ↵Emilio Jesus Gallego Arias
(fix #9204)
2018-12-17Merge PR #9219: [STM] Fix logic of debug DAG printerEnrico Tassi
2018-12-17Merge PR #9220: Move shallow state logic to the function preparing state for ↵Enrico Tassi
workers
2018-12-17CoqIDE: Restoring configuration of default width/height of main window.Hugo Herbelin
Also removing dead code about show_toolbar: this is governed by an item of the view menu rather than by the preference panel since aa357d601 (Dec 2003).
2018-12-16Merge PR #9172: [proof] Rework proof interface.Pierre-Marie Pédrot
2018-12-15Avoid explicit names in binders for automatic introsJasper Hugunin
2018-12-14Merge PR #9073: [sphinx] No more undocumented objects.Clément Pit-Claudel
2018-12-14[dune] [gitlab] Test OCaml trunk.Emilio Jesus Gallego Arias
We add a job testing the build of Coq with OCaml 4.08 [AKA `trunk`] CoqIDE is not supported in 4.08 due to missing `lablgtk`, also `oUnit` cannot be currently installed, thus we have to add a switch to the test suite to disable `unit-tests`. Many deprecation warnings happened in 4.08 so we use the `release` profile to make them not fatal. Using a 4.08 build profile would be an option too.
2018-12-14Merge PR #9147: [dune] [doc] Support for building the reference manual with ↵Théo Zimmermann
Dune.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:47:06 +0000