coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Revert "Better Arguments compatibility."	Maxime Dénès	2016-11-03
*	Merge branch 'v8.6' into trunk	Maxime Dénès	2016-11-03
\|\
\| *	Merge remote-tracking branch 'github/pr/341' into v8.6	Maxime Dénès	2016-11-03
\| \|\
* \| \|	updating ".merlin" file	Matej Kosik	2016-11-03
\| \| *	Better Arguments compatibility.	Maxime Dénès	2016-11-02
\| \|/
* \|	Moving unused code out of the kernel into Termops.	Pierre-Marie Pédrot	2016-10-31
* \|	Stronger static invariant in equality upto universes.	Pierre-Marie Pédrot	2016-10-31
* \|	Code factorization in Universes.	Pierre-Marie Pédrot	2016-10-31
* \|	Moving Universes to the engine/ folder.	Pierre-Marie Pédrot	2016-10-30
* \|	Reordering Termops w.r.t. Evd and Namegen in engine folder.	Pierre-Marie Pédrot	2016-10-30
\| *	Fix spurious OCaml Warning 56 in TACTIC EXTEND macros.	Pierre-Marie Pédrot	2016-10-30
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\\|
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-29
\| \|\
\| * \|	Removing dead code.	Hugo Herbelin	2016-10-29
\| * \|	Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c).	Hugo Herbelin	2016-10-29
\| * \|	Fixing #5164 (regression in locating error in argument of "refine").	Hugo Herbelin	2016-10-29
\| * \|	Merge remote-tracking branch 'github/pr/321' into v8.6	Maxime Dénès	2016-10-28
\| \|\ \
\| * \ \	Merge remote-tracking branch 'github/pr/319' into v8.6	Maxime Dénès	2016-10-28
\| \|\ \ \
\| * \ \ \	Merge commit 'fccbd64' into v8.6	Maxime Dénès	2016-10-28
\| \|\ \ \ \
\| \| * \| \| \|	[build] Add a target to install the META file.	Emilio Jesus Gallego Arias	2016-10-28
\| \| * \| \| \|	[build] META file to enable plugin linking with ocamlfind.	Emilio Jesus Gallego Arias	2016-10-28
\| * \| \| \| \|	Merge remote-tracking branch 'github/pr/337' into v8.6	Maxime Dénès	2016-10-28
\| \|\ \ \ \ \
\| \| \| \| \| \| *	Fixing #5161 (case of a notation with unability to detect a recursive binder).	Hugo Herbelin	2016-10-27
* \| \| \| \| \| \|	COMMENT: unfortunatelly, ocamldoc does not recognize this kind of markup: it ...	Matej Kosik	2016-10-27
\| \| * \| \| \| \|	Add missing dot to impargs error message.	Maxime Dénès	2016-10-27
\| \| * \| \| \| \|	Proper fix for #3753 (anomaly with implicit arguments and renamings)	Maxime Dénès	2016-10-27
\| \| * \| \| \| \|	Complete overhaul of the Arguments vernacular.	Maxime Dénès	2016-10-27
\| * \| \| \| \| \|	Using msg_info for info_auto and info_eauto (PR #324).	Hugo Herbelin	2016-10-26
\| * \| \| \| \| \|	STM: make ~valid state id non optional from APIs	Enrico Tassi	2016-10-26
\| * \| \| \| \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-26
\| \|\ \ \ \ \ \ \| \| \| \|_\|_\|_\|/ \| \| \|/\| \| \| \|
* \| \| \| \| \| \|	COMMENT: Namegen.next_ident_away	Matej Kosik	2016-10-26
* \| \| \| \| \| \|	COMMENT: Declarations.constant_def	Matej Kosik	2016-10-26
* \| \| \| \| \| \|	COMMENT: Names.Cmap and Names.Cmap_env	Matej Kosik	2016-10-26
* \| \| \| \| \| \|	COMMENT: Proofview.entry	Matej Kosik	2016-10-26
* \| \| \| \| \| \|	COMMENT: Constr.kind_of_term	Matej Kosik	2016-10-26
\| \| * \| \| \| \|	Merge remote-tracking branch 'github/pr/338' into v8.5	Maxime Dénès	2016-10-25
\| \| \|\ \ \ \ \
\| \| \| * \| \| \| \|	Remove warning now that info_auto is fixed.	Théo Zimmermann	2016-10-25
\| \| * \| \| \| \| \|	Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."	Maxime Dénès	2016-10-25
\| \| \|/ / / / /
\| * \| \| \| \| \|	Merge commit 'a799600' into v8.6	Maxime Dénès	2016-10-25
\| \|\ \ \ \ \ \
\| \| * \| \| \| \| \|	That Function is unable to create a Fixpoint equation is a user problem,	Yves Bertot	2016-10-25
\| \| \| * \| \| \| \|	Update CHANGES.	Maxime Dénès	2016-10-25
\| \| \| * \| \| \| \|	Bump version number to 8.5pl3.	Maxime Dénès	2016-10-25
\| \| \| * \| \| \| \|	Merge remote-tracking branch 'github/pr/333' into v8.5	Maxime Dénès	2016-10-25
\| \| \| \|\ \ \ \ \
\| \| \| * \ \ \ \ \	Merge remote-tracking branch 'github/pr/329' into v8.5	Maxime Dénès	2016-10-25
\| \| \| \|\ \ \ \ \ \
* \| \| \| \| \| \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-24
\|\\| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-24
\| \|\ \ \ \ \ \ \ \ \ \| \| \| \|/ / / / / / / \| \| \|/\| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	Adding a test for #4398 (interpretation scopes for "match goal").	Hugo Herbelin	2016-10-24
\| * \| \| \| \| \| \| \| \|	Rename lia.cache into .lia.cache in the test-suite Makefile.	Maxime Dénès	2016-10-24
\| * \| \| \| \| \| \| \| \|	Merge commit '81bdc22' into v8.6	Maxime Dénès	2016-10-24
\| \|\ \ \ \ \ \ \ \ \
\| \| \| * \ \ \ \ \ \ \	Merge remote-tracking branch 'github/pr/326' into v8.5	Maxime Dénès	2016-10-24
\| \| \| \|\ \ \ \ \ \ \ \