coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-02-04	Remove `unsafe_type_of` from `Coercion`	Maxime Dénès
	We thread explicitly the evar map everywhere for this purpose.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-05-23	Fixing typos - Part 3	JPR

2018-05-04	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias
	In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2017-05-29	Pretyping cleanup: remove constr_of_global calls	Matthieu Sozeau

2017-02-14	Cases API using EConstr.	Pierre-Marie Pédrot

2017-02-14	Coercion API using EConstr.	Pierre-Marie Pédrot

2016-06-29	Program: cleanup in cases, add options	Matthieu Sozeau
	Unset Program Generalized Coercion to avoid coercion of general applications. Unset Program Cases to deactivate generation equalities and disequalities of cases.
2016-06-27	Rework treatment of default transparency of obligations	Matthieu Sozeau
	By default obligations defined by tactics are defined transparently or opaque according to the Obligations Transparent flag, except proofs of subset obligations which are treated as opaque by default. When the user proves the obligation using Qed or Defined, this information takes precedence, and only when the obligation cannot be Qed'ed because it contains references to a recursive function an error is raised (this prevents the guardness checker error). Shrinked obligations were not doings this correctly. Forcing transparency due to fixpoint prototypes takes precedence over the user preference. Program: do not force opacity of subset proofs, maintaining compatibility.
2016-01-20	Update copyright headers.	Maxime Dénès

2015-01-12	Update headers.	Maxime Dénès

2014-05-06	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau
	latent universes. Now the universes in the type of a definition/lemma are eagerly added to the environment so that later proofs can be checked independently of the original (delegated) proof body. - Fixed firstorder, ring to work correctly with universe polymorphism. - Changed constr_of_global to raise an anomaly if side effects would be lost by turning a polymorphic constant into a constr. - Fix a non-termination issue in solve_evar_evar. -
2012-08-08	Updating headers.	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-25	Added a .mli to pretyping/program.ml	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15490 85f007b7-540e-0410-9357-904b9bb8a0f7