aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-09-12Merge PR #8243: Remove xargs from "make clean" so it won't fail on CygwinEnrico Tassi
2018-09-12Merge PR #8433: Fix bug #8432 : program fixpoint and universesPierre-Marie Pédrot
2018-09-12Merge PR #8372: Grammar rule in the documentation of ssreflect's anonymous ↵Théo Zimmermann
arguments
2018-09-12Merge PR #8406: building-a-coq-project-with-coq-makefile:fix typosThéo Zimmermann
2018-09-11Merge PR #8444: Bump version number to 8.10+alpha.Emilio Jesus Gallego Arias
2018-09-11building-a-coq-project-with-coq-makefile:fix typosJason Gross
make make-pretty-timed- after -> make make-pretty-timed-after (remove space between - and after) (and reflow paragraph) Fix spacing around :: in print-pretty-single-time-diff Closes #8396
2018-09-11Made names of existential variables interpretable as Ltac variables.Hugo Herbelin
This concerns e.g. "?[id]", "?[?id]" or "?id" (in terms, not in patterns), so that all names occurring in terms are consistently interpreted as ltac names. Moreover, with that, we can for instance do: Ltac pick x := eexists ?[x]. Goal exists x, x = 0. pick foo.
2018-09-11Merge remote-tracking branch 'herbelin/master+globenv-coq-pr7288'Pierre-Marie Pédrot
2018-09-11Merge PR #7288: Isolating ltac naming out of pretyping + fixing renamingPierre-Marie Pédrot
2018-09-11Merge PR #8285: Fixing #8270: cbn was applying zeta even when not asked for.Pierre-Marie Pédrot
2018-09-11Merge PR #8278: Do not inline let-bound functions in clambda optimization.Maxime Dénès
2018-09-11Merge PR #8284: [ssr] anomaly -> errorMaxime Dénès
2018-09-11Grammar entry for the ssr syntax for anonymous arguments.Assia Mahboubi
2018-09-11Merge PR #8425: Deprecate romega in favor of liaPierre-Marie Pédrot
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-10Bump version number to 8.10+alpha.Guillaume Melquiond
2018-09-10[dune] Add apidoc target using `odoc`Emilio Jesus Gallego Arias
We build the `@doc` target in the `dune` job: - The documentation can be found in `_build/default/_doc/` - We had to fix a couple of quoting problems.
2018-09-10[ci] [docker] Add more dependencies for Dune-aware jobs.Emilio Jesus Gallego Arias
- odoc: used to generate the ML API documentation by Dune's `@doc` target. - dune-release: Automatic OPAM package generation and release. Both packages require OCaml >= 4.02 thus installing on edge switches only.
2018-09-10Ltac2 overlay.Hugo Herbelin
2018-09-10Relying on the precomputation of the renaming also for new_evar_type.Hugo Herbelin
2018-09-10Fixing ltac names interpretation in internals of pattern-matching compilation.Hugo Herbelin
The parts of pattern-matching compilation which generated names may generate names which collided with names of the Ltac environment. We fix it by avoiding the names of the Ltac environment.
2018-09-10Fixing an inconsistency in interpreting Ltac names linking to binder names.Hugo Herbelin
The recursion names in fix and cofix were not renamed like other binders were.
2018-09-10Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.Hugo Herbelin
This module contains: - the former ExtraEnv in pretyping - a few functions to traverse binders in pretyping.ml and cases.ml - the part of pretyping dealing with genarg interpretation The dependency of pretyping in an interpretation of names as names of variables of identifier is now hidden in GlobEnv (no more explicit "lvar" management in pretyping.ml). Similarly for the interpretation of names as terms and for the interpretation of tactics-in-terms. We keep empty_lvar in Glob_ops for compatibility, even though it is a bit isolated there.
2018-09-10Temptative clarification of the role of ltac_genargs field in ltac_var_map.Hugo Herbelin
2018-09-10Minor cosmetic unifying of layout in pretyping.ml.Hugo Herbelin
2018-09-10Files pretyping.ml, glob_obs.ml, evarutil.ml: rewording/typos in some comments.Hugo Herbelin
2018-09-10Deprecate romega in favor of lia.Vincent Laporte
2018-09-07Bvector: add BVeq and some notationsYishuai Li
2018-09-07NArith: deprecate N2Bv_genYishuai Li
Use N2Bv_sized instead.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-02 18:29:33 +0000