coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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.