coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
\| \| \| \| \| \| \| \| \| \| \| \| \|	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.
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Pretyping cleanup: remove constr_of_global calls	Matthieu Sozeau	2017-05-29
\|
*	Cases API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Coercion API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|
*	Program: cleanup in cases, add options	Matthieu Sozeau	2016-06-29
\| \| \| \| \| \| \|	Unset Program Generalized Coercion to avoid coercion of general applications. Unset Program Cases to deactivate generation equalities and disequalities of cases.
*	Rework treatment of default transparency of obligations	Matthieu Sozeau	2016-06-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
\| \| \| \| \| \| \| \| \| \| \| \|	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. -
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a .mli to pretyping/program.ml	ppedrot	2012-06-25
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15490 85f007b7-540e-0410-9357-904b9bb8a0f7