coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Add an invariant on future goals in Proof.run_tactic.	Hugo Herbelin	2018-03-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	More precisely, we check that future goals retrieved in run_tactic have no given_up goals since given_up goals are supposed to be produced only by Proofview.given_up and put on the given_up store. Doing the same for the shelf does not work: there is a situation where run_tactic ends where the same goal is both in the comb and on the shelf. This is when calling "clear x" on a goal "x:A \|- ?p:B(?q[x])" when the dependent goal "x:A \|- ?q:C" is not on the shelf. Tactic "clear" creates "\|- ?p':B(?q'[])" and "\|- ?q':C". The "advance" thing sees that the new comb is now composed of ?p' and ?q' but ?q' is a future goal which is later collected on the shelf (which ?q' is also in the comb). I tried to remove this redundancy but apparently it is necessary. There is an example in HoTT (file Classes/theory/rational.v) which requires this redundancy. I did not investigate why: the dependent evar is created by ring as part of a big term. So, as a conclusion, I kept the redundancy.
*	Add an invariant on given up goals in class_tactics.	Hugo Herbelin	2018-03-08
\|
*	Proof engine: support for nesting tactic-in-term within other tactics.	Hugo Herbelin	2018-03-08
\| \| \| \| \| \| \| \| \| \| \| \| \|	Tactic-in-term can be called from within a tactic itself. We have to preserve the preexisting future_goals (if called from pretyping) and we have to inform of the existence of pending goals, using future_goals which is the only way to tell it in the absence of being part of an encapsulating proofview. This fixes #6313. Conversely, future goals, created by pretyping, can call ltac:(giveup) or ltac:(shelve), and this has to be remembered. So, we do it.
*	Adding tclPUTGIVENUP/tclPUTSHELF in Proofview.Unsafe.	Hugo Herbelin	2018-03-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Adding also tclSETSHELF/tclGETSHELF by consistency with tclSETGOALS/tclGETGOALS. However, I feel that this is too low-level to be exported as a "tcl". Doesn't a "tcl" mean that it is supposed to be used by common tactics? But is it reasonable that a common tactic can change and modify comb and shelf without passing by a level which e.g. checks that no goal is lost in the process. So, I would rather be in favor of removing tclSETGOALS/tclGETGOALS which are anyway aliases for Comb.get/Comb.set. Conversely, what is the right expected level of abstraction for proofview.ml?
*	Add function bind in option.ml.	Hugo Herbelin	2018-03-08
\|
*	Proof engine: using save_future_goal when relevant.	Hugo Herbelin	2018-03-08
\|
*	Proof engine: adding a function to save future goals including principal one.	Hugo Herbelin	2018-03-08
\|
*	Proof engine: consider the pair principal and future goals as an entity.	Hugo Herbelin	2018-03-08
\|
*	Merge PR #6522: Fix core hint database issue #6521	Maxime Dénès	2018-03-08
\|\
* \	Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials	Maxime Dénès	2018-03-08
\|\ \
* \ \	Merge PR #6928: gitlab: install num for all 4.06 jobs	Maxime Dénès	2018-03-08
\|\ \ \
* \ \ \	Merge PR #6926: An experimental 'Show Extraction' command (grant feature ↵	Maxime Dénès	2018-03-08
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	wish #4129)
* \ \ \ \	Merge PR #6893: Cleanup UState API usage	Maxime Dénès	2018-03-08
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6918: romega: get rid of EConstr.Unsafe	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6817: [configure]: support for profiles	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6743: Add notation {x & P} for sigT	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6927: Add some missing flushes in configure.	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6909: Deprecate Focus and Unfocus	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6899: [compat] Remove "Standard Proposition Elimination"	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6881: [windows] support -addon in build script	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6582: Mangle auto-generated names	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6933: Standard headers for C and Python.	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6934: Warn when using “Require” in a section	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6924: Clean-up remove always false useeager argument.	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6902: [compat] Remove "Discriminate Introduction"	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6903: [compat] Remove "Shrink Abstract"	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)	Maxime Dénès	2018-03-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	gitlab: install num for all jobs	Gaëtan Gilbert	2018-03-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Previously it was installed for the compilation jobs causing random failures when the other jobs got a cache without it.
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Use a proper warning when a summary is captured out of module scope.	Vincent Laporte	2018-03-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[vernac] Warn when using “Require” in a section	Vincent Laporte	2018-03-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[stdlib] Do not use “Require” inside sections	Vincent Laporte	2018-03-07
\| \|_\|_\|_\|/ / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6744: Add String.concat	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6932: [stdlib] Do not use deprecated notations	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6905: Fix make ml-doc	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6922: Remove outdated information regarding the FAQ.	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6374: [toplevel] Modify printing goal strategy.	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6790: Allow universe declarations for [with Definition].	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	An experimental 'Show Extraction' command (grant feature wish #4129)	Pierre Letouzey	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Attempt to extract the current ongoing proof (request by Clément Pit-Claudel on coqdev, and also #4129). Evars are handled as axioms.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Extraction: switch to EConstr.t as the central type to extract from.	Pierre Letouzey	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is a bit artificial since the extraction normally operates on finished constrs (with no evars). But: - Since we use Retyping quite a lot, switching to EConstr.t allows to get rid of many `EConstr.Unsafe.to_constr (... (EConstr.of_constr ...))` - This prepares the way for a possible extraction of the content of ongoing proofs (a forthcoming `Show Extraction` command, see #4129 )
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	romega: get rid of EConstr.Unsafe	Pierre Letouzey	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/ / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We replace constr by EConstr.t everywhere, and propagate some extra sigma args
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	document -profile in dev/doc/setup.txt	Enrico Tassi	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Standard headers for C and Python.	Maxime Dénès	2018-03-06
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[stdlib] Do not use deprecated notations	Vincent Laporte	2018-03-06
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Add some missing flushes in configure.	Maxime Dénès	2018-03-06
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Some messages were sometimes not printed because of the missing flushes. We use a generic combinator suggested by Emilio.
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Hack to make bignum build on windows	Enrico Tassi	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	build: win: turn off build/installation of gnu Make	Enrico Tassi	2018-03-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Clean-up remove always false useeager argument.	Théo Zimmermann	2018-03-06
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Remove outdated information regarding the FAQ.	Théo Zimmermann	2018-03-06
\| \|_\|_\|/ / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The FAQ is not part of the Coq sources anymore.