aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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-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-07Fix bug #8432 : program fixpoint and universesMatthieu Sozeau
One didn't normalize the bodies of fixpoints according to the universe context, resulting in a type errors. Use EConstr.to_constr to ensure universes are normalized instead of using EConstr.Unsafe.to_constr.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 03:44:37 +0000