coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-12
\|
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-12
\|
*	Merge remote-tracking branch 'github/pr/263' into v8.6	Maxime Dénès	2016-10-03
\|\ \| \| \| \| \| \|	Was PR#263: Fast lookup in named contexts
* \|	Adding variants enter_one and refine_one which assume that exactly one	Hugo Herbelin	2016-09-16
\| \| \| \| \| \| \| \|	goal is under focus and which support returning a relevant output.
\| *	Tracking careless uses of slow name lookup.	Pierre-Marie Pédrot	2016-09-09
\|/
*	Fast path in push_rel_context_to_named_context.	Pierre-Marie Pédrot	2016-09-05
\| \| \| \| \|	Essentially, we do not reconstruct the named_context_val when the rel_context is empty.
*	Fast path in whd_evar.	Pierre-Marie Pédrot	2016-09-02
\| \| \| \| \|	Before computing the whd_evar-form of the arguments of an evar, we first check that it is indeed defined.
*	Short documentation, filling TODO's in evd.mli.	Hugo Herbelin	2016-09-01
\|
*	Do not export an internal function in Namegen.	Pierre-Marie Pédrot	2016-08-25
\|
*	Two protections against failures when printing evar_map.	Hugo Herbelin	2016-08-17
\| \| \| \| \| \| \| \|	Delimit the scope of the failure to ease potential need for debugging the debugging printer. Protect against one of the causes of failure (calling get_family_sort_of with non-synchronized sigma).
*	Fixing printing in debugger (no global env in debugger).	Hugo Herbelin	2016-08-17
\|
*	Efficiently generate the pretyping contexts.	Pierre-Marie Pédrot	2016-08-16
\|\ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We used to recompute all fresh named contexts for evars before this patch in the push_rel_context_to_named_context function. This was incurring a linear penalty and a memory explosion due to the reallocation of many arrays. Now, we rather remember the context between evar creations by sharing it in the pretyping environment. This can be considered as a fix for bug #4964 even though we might do better.
* \|	Remove unused optional "predicative" argument.	Guillaume Melquiond	2016-08-10
\| \|
\| *	Using a dedicated kind of substitutions in evar name generation.	Pierre-Marie Pédrot	2016-08-06
\| \| \| \| \| \| \| \|	This saves a quadratic allocation by replacing arrays with maps.
\| *	Using the extended contexts in pretyping.	Pierre-Marie Pédrot	2016-08-05
\| \| \| \| \| \| \| \| \| \|	In addition to sharing, we also delay the computation of the environment in a by-need fashion.
\| *	Use sets instead of lists for names to avoid in evar generation.	Pierre-Marie Pédrot	2016-08-04
\| \|
\| *	Simplifying code in evar generation.	Pierre-Marie Pédrot	2016-08-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove in particular a dubious use of an environment in fresh name generation. The code was using the wrong environment in a function only depending on the rel context which was resetted most of the time. This might change the generated names in extremely rare occurences.
\| *	Exporting the renaming API for evar declaration.	Pierre-Marie Pédrot	2016-08-04
\|/
*	Fixing #4906 (regression in printing an error message).	Hugo Herbelin	2016-07-08
\|
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey	2016-07-03
\| \| \| \| \| \|	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
*	Univ: Use loc even if there are more unbound levels	Matthieu Sozeau	2016-06-29
\|
*	Univs: add source locations of levels	Matthieu Sozeau	2016-06-29
\| \| \| \| \|	For better error messages. The API change is backwards compatible, using a new optional argument.
*	Optmimize the subst tactic.	Pierre-Marie Pédrot	2016-06-24
\| \| \| \|	Take advantage that the provided term is always a variable in Equality.is_eq_x.
*	Optimize the clear tactic.	Pierre-Marie Pédrot	2016-06-24
\| \| \| \|	We do not allocate a closure in the main loop, and do so only when needed.
*	Optimize the clear tactic.	Pierre-Marie Pédrot	2016-06-24
\| \| \| \| \|	We do not check for presence of a variable in a global definition when we know that this variable was not present in the section.
*	Better algorithm for variable deambiguation in term printing.	Pierre-Marie Pédrot	2016-06-23
\| \| \| \| \| \| \| \| \|	We do not recompute shortest name identifier for global references that were already traversed. Furthermore, we share the computation of identifiers between invokations of the name generating function. This drastically speeds up detyping for huge goals, further mitigating the shortcomings of the fix for bug #4777.
*	Document new Hint Mode option.	Matthieu Sozeau	2016-06-16
\|
*	Proofview: extensions for backtracking eauto	Matthieu Sozeau	2016-06-16
\| \| \| \| \| \| \| \| \| \|	unshelve_goals is used to correctly register dependent subgoals that have to be solved. Resolution may fail to do so using hints, so we have to put them back as goals in that case. The shelf is a good interface for doing that. unifiable can be used outside proofview to detect dependencies between goals. This might be better in another module.
*	Implement limited proof search and iterative deepening.	Matthieu Sozeau	2016-06-16
\| \| \| \|	Fix typo in proofview
*	Merge 'pr/191' into trunk	Enrico Tassi	2016-06-16
\|\
* \	Merge remote-tracking branch 'origin/pr/173' into trunk	Enrico Tassi	2016-06-14
\|\ \ \| \| \| \| \| \| \| \| \|	This is the "error resiliency" mode for STM
\| \| *	Fix a typo in proofs/proofview.mli.	Cyprien Mangin	2016-06-14
\| \| \|
\| \| *	Fix usage of Pervasives in goal selectors.	Cyprien Mangin	2016-06-14
\| \| \|
\| \| *	Add a comment about the use of a zipper, for clarity.	Cyprien Mangin	2016-06-14
\| \| \|
\| \| *	Add a [CList.partitioni] function.	Cyprien Mangin	2016-06-14
\| \| \|
\| \| *	Add goal range selectors.	Cyprien Mangin	2016-06-14
\| \|/ \|/\| \| \| \| \| \| \|	You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals numbered 1 and 3 to 5.
* \|	Adding a bit of documentation in the mli.	Pierre-Marie Pédrot	2016-06-09
\| \|
\| *	STM: proof block detection for bullets and { block }	Enrico Tassi	2016-06-06
\|/
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-20
\|
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
\|
*	Normalizing the names of dynamic types to follow a typ_* scheme.	Pierre-Marie Pédrot	2016-05-04
\|
*	Interpretation function can return any untyped value.	Pierre-Marie Pédrot	2016-05-04
\|
*	Removing external uses of Val.inject and making Geninterp.interp return Val.t	Pierre-Marie Pédrot	2016-05-04
\|
*	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
\|
*	Getting rid of the Geninterp.generic_interp function.	Pierre-Marie Pédrot	2016-05-04
\|
*	Switching to an untyped toplevel representation for Ltac values.	Pierre-Marie Pédrot	2016-05-04
\|
*	Moving Ftactic and Geninterp to the engine folder.	Pierre-Marie Pédrot	2016-05-04
\|
*	Moving Evarutil and Proofview to engine/	Pierre-Marie Pédrot	2016-03-20
\|
*	Making Proofview independent of Logic.	Pierre-Marie Pédrot	2016-03-20
\|