coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
\| \| \| \| \| \| \|	We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`.
*	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
\| \| \| \| \| \| \| \| \| \| \|	We'd like to handle proofs functionally we thus recommend not to use printing functions without an explicit context. We also adapt most of the code, making more explicit where the printing environment is coming from. An open task is to refactor some code so we gradually make the `Pfedit.get_current_context ()` disappear.
*	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
\|
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
\| \| \| \|	This will allow to merge back `Names` with `API.Names`
*	Himsg: Dropping nf_evars made obsolete by EConstr.	Hugo Herbelin	2017-09-22
\|
*	Cannot unify message: improve preventing repeating twice the same message.	Hugo Herbelin	2017-09-22
\| \| \| \| \|	Call to nf_betaiota was done on one side of the comparison preventing the same message to be repeated twice but not on the other side.
*	Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.	Maxime Dénès	2017-09-15
\|\
\| *	Port is_Set and is_Type to EConstr, as was is_Prop already.	Guillaume Melquiond	2017-09-12
\| \|
* \|	Fixing a capitalization in the middle of the sentence of an error message.	Hugo Herbelin	2017-08-30
\|/
*	Detyping functions are now operating on EConstr.t.	Pierre-Marie Pédrot	2017-08-01
\| \| \| \|	This was already the case, but the API was not exposing this.
*	Remove a few useless evar-normalizations in printing code.	Pierre-Marie Pédrot	2017-07-26
\|
*	The only abstraction-breaking function in Univ is now AUContext.instance.	Pierre-Marie Pédrot	2017-07-13
\|
*	Properly handling polymorphic inductive subtyping in the kernel.	Pierre-Marie Pédrot	2017-07-11
\| \| \| \| \|	Before this patch, inductive subtyping was enforcing syntactic equality of the variable instance, instead of reasoning up to alpha-renaming.
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
\|
*	Creating a module Nameops.Name extending module Names.Name.	Hugo Herbelin	2017-05-31
\| \| \| \| \| \| \| \| \| \| \| \|	This module collects the functions of Nameops which are about Name.t and somehow standardize or improve their name, resulting in particular from discussions in working group. Note the use of a dedicated exception rather than a failwith for Nameops.Name.out. Drawback of the approach: one needs to open Nameops, or to use long prefix Nameops.Name.
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|
*	[stm] Break stm/toplevel dependency loop.	Emilio Jesus Gallego Arias	2017-02-15
	Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore.