aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-12-19Merge PR #9237: Add Map.find_optPierre-Marie Pédrot
2018-12-19[doc] typoEnrico Tassi
2018-12-19coqchk: fix check for kelim with functorsGaëtan Gilbert
2018-12-19Fix typo in gallina specification language docyudetamago
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 pull request coq/ltac2#91 from ejgallego/proof_reworkPierre-Marie Pédrot
[coq] Adapt to coq/coq#9172
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-14Fix issue: Windows CI: cygwin install cache is not reused #9212Michael Soegtrop
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.
2018-12-14[proof] Rework proof interface.Emilio Jesus Gallego Arias
- deprecate the old 5-tuple accessor in favor of a view record, - move `name` and `kind` proof data from `Proof_global` to `Proof`, this will prove useful in subsequent functionalizations of the interface, in particular this is what abstract, which lives in the monads, needs in order no to access global state. - Note that `Proof.t` and `Proof_global.t` are redundant anyways.
2018-12-14Update pinned nixpkgs to use Dune 1.6.Théo Zimmermann
2018-12-14Turn warning on for undocumented objects. Closes #7602.Théo Zimmermann
2018-12-14Fix the SSReflect chapter regarding objects without bodies.Théo Zimmermann
2018-12-14Do not raise object without body warning for prodn objects.Théo Zimmermann
2018-12-13Merge PR #9193: Tests for #4509, #6202 which happen to be fixed (was a lost ↵Gaëtan Gilbert
of evars in shelf)
2018-12-13Merge PR #9194: Fixing uses of sed in #8985 which do not work on MacOS XMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 23:37:43 +0000