coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-03-12	Move the responsibility of type-checking to the caller for tactic-in-terms.	Pierre-Marie Pédrot
	Instead of taking a type and checking that the inferred type for the expression is correct, we simply pick an optional constraint and return the type directly in the callback. This prevents having to compute type conversion twice in the special case of Ltac2 variable quotations. This should be 1:1 equivalent to the previous code, we are just moving code around.
2020-08-06	Actually use the default instance stored inside named_context_val.	Pierre-Marie Pédrot

2020-07-08	Remove Evarutil.new_evar_instance from the API.	Pierre-Marie Pédrot

2020-06-19	Share the identity instance in pretyping environments.	Pierre-Marie Pédrot

2020-06-19	Do not reallocate named_context_val of the pretyping environment.	Pierre-Marie Pédrot
	Instead of costly linear reallocations, we share as much as possible of the prefixes of the various environment subcomponents.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-10-21	Fixes #10894: uconstr was not anymore typed in the Ltac-substituted environment.	Hugo Herbelin
	More precisely: The equivalent in #7288 (4dab4fc) to the former call to ltac_interp_name_env was not done anymore when interpreting uconstr's.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-03-27	[geninterp] Track polymorphic status in tactic interpretation.	Emilio Jesus Gallego Arias

2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
	Kernel should be mostly correct, higher levels do random stuff at times.
2019-02-05	Make Program a regular attribute	Maxime Dénès
	We remove all calls to `Flags.is_program_mode` except one (to compute the default value of the attribute). Everything else is passed explicitely, and we remove the special logic in the interpretation loop to set/unset the flag. This is especially important since the value of the flag has an impact on proof modes, so on the separation of parsing and execution phases.
2018-10-03	[pretyper] Remove imperative passing of evar_map.	Emilio Jesus Gallego Arias

2018-09-26	[print] Restrict use of "debug" Termops printer.	Emilio Jesus Gallego Arias
	The functions in `Termops.print_*` are meant to be debug printers, however, they are sometimes used in non-debug code due to a API confusion. We thus wrap such functions into an `Internal` module, improve documentation, and switch users to the right API.
2018-09-11	Made 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-10	Relying on the precomputation of the renaming also for new_evar_type.	Hugo Herbelin

2018-09-10	Fixing 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-10	Moving 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.