coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge remote-tracking branch 'origin/v8.5' into trunk	Hugo Herbelin	2015-09-09
\|\
\| *	Documenting the code when preference is given to expansion of default	Hugo Herbelin	2015-09-08
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-08-05
\|\\|
\| *	Continuing 817308ab (use ltac env for terms in ltac context) + fix	Hugo Herbelin	2015-08-02
\| *	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
\| *	Documenting in passing.	Hugo Herbelin	2015-08-02
\| *	Hopefully clearer printing of stack when debugging evarconv unification.	Hugo Herbelin	2015-08-02
\| *	Cosmetic changes in evarconv.ml: hopefully more regular names and form	Hugo Herbelin	2015-08-02
\| *	Cosmetic changes in evarconv.ml: hopefully more regular form and	Hugo Herbelin	2015-08-02
\| *	Cosmetic changes in evarconv.ml: hopefully using better self-documenting names.	Hugo Herbelin	2015-08-02
\| *	Evarconv.ml: small cut-elimination, saving useless zip.	Hugo Herbelin	2015-08-02
\| *	Cosmetic in evarconv.ml: naming a local function for better readibility.	Hugo Herbelin	2015-08-02
\| *	Fixing #4221 (interpreting bound variables using ltac env was possibly	Hugo Herbelin	2015-08-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-27
\|\\|
\| *	Fixing bug #4303: Anomaly: Uncaught exception Invalid_argument.	Pierre-Marie Pédrot	2015-07-21
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-18
\|\\|
\| *	Refining 71def2f8 on too strong occur-check limiting evar-evar	Hugo Herbelin	2015-07-16
\| *	Slight improvement in naming anonymous variables in error messages:	Hugo Herbelin	2015-07-16
\| *	Fixing #4177 (find_projectable was liable to ask to instantiate an evar twice).	Hugo Herbelin	2015-07-16
\| *	Fixing bug #4240 (closure_of_filter was not ensuring refinement of	Hugo Herbelin	2015-07-16
\| *	Fix universe instantiation with canonical structures.	Maxime Dénès	2015-07-16
\| *	Continuing 93579407, spotting other potential sources of anomaly	Hugo Herbelin	2015-07-16
\| *	Fixing anomaly #3743 while printing an error message involving evar constraints.	Hugo Herbelin	2015-07-16
\| *	Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72.	Hugo Herbelin	2015-07-10
\| *	Option -type-in-type: added support in checker and making it contaminating	Hugo Herbelin	2015-07-10
\| *	Make retyping of projections more resilient to wrong environment.	Maxime Dénès	2015-07-09
\| *	Univs: bug fix.	Matthieu Sozeau	2015-07-07
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-07-06
\|\\|
\| *	Fix handling of primitive projections in VM.	Maxime Dénès	2015-07-05
\| *	Assumptions: more informative print for False axiom (Close: #4054)	Enrico Tassi	2015-06-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-28
\|\\|
\| *	Fix incompleteness of conversion used by evarconv	Matthieu Sozeau	2015-06-28
\| *	Fix bug #4254 with the help of J.H. Jourdan	Matthieu Sozeau	2015-06-26
* \|	Merge remote-tracking branch 'forge/v8.5'	Pierre Boutillier	2015-06-22
\|\\|
\| *	Make normalization of primitive projections in native_compute the same as wit...	Maxime Dénès	2015-06-08
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-01
\|\\|
\| *	Fixup for 866c41b	Enrico Tassi	2015-05-28
\| *	Fix bug #4159	Matthieu Sozeau	2015-05-27
\| *	Adding an extensible global state to evarmaps.	Pierre-Marie Pédrot	2015-05-19
\| *	Make Coercion.inh_app_fun respect its specification.	Pierre-Marie Pédrot	2015-05-15
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	Disable precompilation for native_compute by default.	Guillaume Melquiond	2015-05-14
\| *	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
\| *	Fix for a second avatar of bug #4234.	Pierre-Marie Pédrot	2015-05-13
\| *	Better fixing #4198 such that the term to match is looked for before	Hugo Herbelin	2015-05-13
\| *	Fixing bug #4234.	Pierre-Marie Pédrot	2015-05-12
\| *	Code factorization in Constr_matching.	Pierre-Marie Pédrot	2015-05-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
\| *	Tactical `progress` compares term up to potentially equalisable universes.	Arnaud Spiwack	2015-04-22