coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7789: Fixes #7779: destruct's "in" clause was forgetting the possib...	Pierre-Marie Pédrot	2018-06-13
\|\
\| *	Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").	Hugo Herbelin	2018-06-12
* \|	[api] Remove Misctypes.	Emilio Jesus Gallego Arias	2018-06-12
* \|	[api] Misctypes removal: tactic flags.	Emilio Jesus Gallego Arias	2018-06-12
* \|	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
* \|	[api] Misctypes removal: multi to tactics/rewrite	Emilio Jesus Gallego Arias	2018-06-12
\|/
*	Merge PR #7629: Fix anomaly in autoapply when an unbound hint name is provided	Matthieu Sozeau	2018-06-07
\|\
* \	Merge PR #6874: [econstr] Some minor tweaks	Pierre-Marie Pédrot	2018-06-07
\|\ \
* \ \	Merge PR #7004: Make `simple apply` obey `Opaque` directive.	Pierre-Marie Pédrot	2018-06-05
\|\ \ \
* \ \ \	Merge PR #7099: Stronger invariants in unification signature.	Matthieu Sozeau	2018-06-05
\|\ \ \ \
\| \| * \| \|	Make direct invocations of `simple apply` obey `Opaque` directive.	Maxime Dénès	2018-06-05
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-	Pierre-Marie Pédrot	2018-06-04
\|\ \ \ \
\| \| \| * \|	[econstr] Remove some Unsafe.to_constr use.	Emilio Jesus Gallego Arias	2018-06-04
\| \|_\|/ / \|/\| \| \|
\| \| * \|	Stronger invariants in unification signature.	Pierre-Marie Pédrot	2018-06-04
\| \|/ / \|/\| \|
* \| \|	Merge PR #7216: Replace uses of Termops.dependent by more specific functions.	Matthieu Sozeau	2018-06-04
\|\ \ \
* \ \ \	Merge PR #7249: Cleaning, documentation, uniformisation of the Coq extension ...	Pierre-Marie Pédrot	2018-06-04
\|\ \ \ \
* \ \ \ \	Merge PR #7640: Small refactoring to clarify make_local_hint_db.	Pierre-Marie Pédrot	2018-06-04
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7649: Remove some dead code in class_tactics.ml	Pierre-Marie Pédrot	2018-06-04
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7637: Fix an outdated comment refering to lib/dnet.mli	Pierre-Marie Pédrot	2018-06-03
\|\ \ \ \ \ \ \
\| \| \| \| * \| \| \|	Cleaning, documentation, uniformisation of the Coq extension of List.	Hugo Herbelin	2018-06-03
\| \|_\|_\|/ / / / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #7234: Reduce circular dependency constants <-> projections	Maxime Dénès	2018-06-01
\|\ \ \ \ \ \ \
\| \| \| * \| \| \| \|	Remove some dead code in class_tactics.ml	Armaël Guéneau	2018-05-31
\| \|_\|/ / / / / \|/\| \| \| \| \| \|
\| \| \| \| \| * \|	Refactor parsing rules for Hint Resolve -> and Hint Resolve <-	Armaël Guéneau	2018-05-31
\| \|_\|_\|_\|/ / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6969: [api] Remove functions deprecated in 8.8	Maxime Dénès	2018-05-31
\|\ \ \ \ \ \
\| \| * \| \| \| \|	Reduce circular dependency constants <-> projections	Gaëtan Gilbert	2018-05-31
* \| \| \| \| \| \|	Move interning the [hint_pattern] outside the Typeclasses hooks.	Gaëtan Gilbert	2018-05-30
\| \|/ / / / / \|/\| \| \| \| \|
\| * \| \| \| \|	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
\|/ / / / /
* \| \| \| \|	Merge PR #7558: [api] Make `vernac/` self-contained.	Maxime Dénès	2018-05-30
\|\ \ \ \ \
\| \| \| * \| \|	Small refactoring to clarify make_local_hint_db.	Théo Zimmermann	2018-05-30
\| \| * \| \| \|	Fix an outdated comment refering to lib/dnet.mli	Armaël Guéneau	2018-05-30
\| \| \|/ / /
\| \| \| \| *	Fix anomaly in autoapply when an unbound hint name is provided	Armaël Guéneau	2018-05-29
\| \| \| \|/ \| \| \|/\|
* \| / \|	Tactics.introduction: remove dangerous option ~check	Enrico Tassi	2018-05-28
\| \|/ / \|/\| \|
\| * \|	[api] Make `vernac/` self-contained.	Emilio Jesus Gallego Arias	2018-05-27
\| * \|	[tactics] Turn boolean locality hint parameter into a named one.	Emilio Jesus Gallego Arias	2018-05-27
* \| \|	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
\|/ /
* \|	[tactics] Remove anonymous fix/cofix form.	Emilio Jesus Gallego Arias	2018-05-24
* \|	Moving Option.smart_map to Option.Smart.map.	Hugo Herbelin	2018-05-23
* \|	Collecting List.smart_* functions into a module List.Smart.	Hugo Herbelin	2018-05-23
* \|	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
* \|	Split off Universes functions about substitutions and constraints	Gaëtan Gilbert	2018-05-17
* \|	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
* \|	Stop using Universes.subst(_opt)_univs_constr	Gaëtan Gilbert	2018-05-17
* \|	Deprecate Typing.e_* functions	Gaëtan Gilbert	2018-05-14
* \|	Deprecate Refiner [evar_map ref] exported functions.	Gaëtan Gilbert	2018-05-14
* \|	Deprecate Evarconv.e_conv,e_cumul	Gaëtan Gilbert	2018-05-11
* \|	Convert clear_hyps_in_evi to state passing style.	Gaëtan Gilbert	2018-05-11
* \|	Deprecate most evarutil evdref functions	Gaëtan Gilbert	2018-05-11
* \|	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
* \|	Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.	Pierre-Marie Pédrot	2018-05-04
\|\ \
* \| \|	Make "intro"/"intros" progress on existential variables.	Hugo Herbelin	2018-05-02