aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-09-11Merge PR #7135: Introducing an explicit `Declare Scope` commandEmilio Jesus Gallego Arias
2018-09-11Merge PR #8452: Fix #8358: circular make dependency for camldevfilesEnrico Tassi
2018-09-11Merge PR #8448: Have `gitFull` in the nix-shellVincent Laporte
2018-09-11Merge PR #8105: Remove environment passing to cache_coercion functionHugo Herbelin
2018-09-10Remove environment passing to coercion printersGaëtan Gilbert
(It's unused after moving coercions to globrefs)
2018-09-10Merge PR #8230: fix formulation of the Euclid Theorem in commentHugo Herbelin
2018-09-10Declaring Scope prior to loading primitive printers.Hugo Herbelin
2018-09-10Documenting "Declare Scope".Hugo Herbelin
2018-09-10CHANGES: mentioning new command "Declare Scope".Hugo Herbelin
2018-09-10Fix #8358: circular make dependency for camldevfilesGaëtan Gilbert
2018-09-10Have `gitFull` in the nix-shellCyril Cohen
2018-09-10Merge PR #8417: Fixing #8416: Print Assumptions missing module information ↵Matthieu Sozeau
from compiles files
2018-09-10Merge PR #8290: Fix #8288: cumulativity inferance ignores args to bound ↵Matthieu Sozeau
variables
2018-09-10Merge PR #7743: Bound proof-search in default program obligation tactic.Pierre-Marie Pédrot
2018-09-10Merge PR #8323: Owners of Makefile.{ci,doc} are teams {ci,doc}-maintainers.Maxime Dénès
2018-09-10Merge PR #8430: Move to a team of code owners for the Nix files.Maxime Dénès
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
Removing in passing two Local which are no-ops in practice.
2018-09-10Support for Local flag in Declare Scope, Undelimit/Delimit Scope, Bind Scope.Hugo Herbelin
This is for use in modules. By default, the behavior is local in sections and Global is forbidden in sections. By default, the behavior is global in modules.
2018-09-10Adding a command "Declare Scope" and deprecating scope implicit declaration.Hugo Herbelin
2018-09-10Merge PR #8104: Warnings on coercions used without being ImportedEnrico Tassi
2018-09-07Merge PR #8437: Recover lost snippetThéo Zimmermann
2018-09-07Merge PR #8435: [dune] Fix build of coq_dune in 4.02.3Théo Zimmermann
2018-09-07Recover lost snippetMatěj G
This snippet on pattern matching got lost in the process of migrating to Sphynx.
2018-09-07Merge PR #8428: Add utop to default.nix for use in nix-shell (see #8426).Vincent Laporte
2018-09-07[dune] Fix build of coq_dune in 4.02.3Emilio Jesus Gallego Arias
Fixes #8431
2018-09-07Warnings on coercions used without being ImportedMaxime Dénès
This warning makes it much easier to stop relying on `Set Automatic Coercions Import`. Tested with success on math-classes.
2018-09-07Merge PR #8423: coqpp: allow DEPRECATED when declaring tacticsPierre-Marie Pédrot
2018-09-07Move to a team of code owners for the Nix files.Théo Zimmermann
2018-09-07Add utop to default.nix for use in nix-shell (see #8426).Théo Zimmermann
2018-09-07Merge PR #8426: [dune] [doc] Document `dune utop $lib`Théo Zimmermann
2018-09-07Merge PR #8411: Changes to default.nix to be able to use Dune.Vincent Laporte
2018-09-06Merge PR #8412: [dune] [ci] Fix and test release profile + use 1.1 ↵Gaëtan Gilbert
dune-workspace
2018-09-06[dune] [doc] Document `dune utop $lib`Emilio Jesus Gallego Arias
2018-09-06[dune] [ci] Fix and test release profile + use 1.1 dune-workspaceEmilio Jesus Gallego Arias
Dune 1.1 allows us to define the `env` flags in the workspace file, which is a better place than the current situation. Along the way, We fix the build flags for release mode [missing `-rectypes` and add a `release` build profile CI job.
2018-09-06Deprecation warning in legacy tacextend.mlpVincent Laporte
2018-09-06deprecation is CODE instead of IDENTVincent Laporte
2018-09-06Bound proof-search in default program obligation tactic.Matthieu Sozeau
This issue was first reported on equations where a definition seemingly took all memory until Coq crashed. https://github.com/mattam82/Coq-Equations/issues/69
2018-09-06coqpp: allow DEPRECATED when declaring tacticsVincent Laporte
2018-09-06Merge PR #8110: Fixing capital letters in the "in" syntax of instantiate.Pierre-Marie Pédrot
2018-09-06Merge PR #8394: Print the entire string to the CoqIDE screen, e.g. for ↵Pierre-Marie Pédrot
"Print Options"
2018-09-06Merge PR #8415: [bin] Fix binary location procedure to work with symlinks.Pierre-Marie Pédrot
2018-09-06Merge PR #8420: [pfedit] Fix master build due to merge conflictGaëtan Gilbert
2018-09-06[pfedit] Fix master build due to merge conflictEmilio Jesus Gallego Arias
2018-09-06Merge PR #8302: Fix #7795: UGraph.AlreadyDeclared with ProgramMatthieu Sozeau
2018-09-06Override Dune derivation to update it before nixpkgs.Théo Zimmermann
As suggested by Vincent.
2018-09-06Changes to default.nix to be able to use Dune.Théo Zimmermann
2018-09-06Merge PR #8295: Fix #8291: print universe names in universe context for Check.Matthieu Sozeau
2018-09-05Fixing #8416 (Print Assumptions missing module information from compiled files).Hugo Herbelin
This fixes the fix 1522b989 to #7192. The remaining Not_found after 1522b989 should have rung a bell that something was still strange.
2018-09-05[bin] Fix binary location procedure to work with symlinks.Emilio Jesus Gallego Arias
In #7860 `Sys.executable_name` was introduced to locate coq private binaries; however, this breaks use cases with symlinks, such as Dune. In order to fix this, we adopt a simpler strategy; we will always adapt the name originally provided by the user, and only add a directory if it was originally present. This should work (hopefully) in all cases. This fixes `coqide` not working on Dune builds.
2018-09-05Merge PR #6857: [build] Preliminary support for building with `dune`.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:15:08 +0000