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-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-05-23	Fixing typos - Part 3	JPR

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-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.