coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-06-16	Proofview: extensions for backtracking eauto	Matthieu Sozeau
	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.
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
	You can now write [[1, 3-5]:tac.] to apply [tac] on the subgoals numbered 1 and 3 to 5.
2016-05-31	Feedback cleanup	Emilio Jesus Gallego Arias
	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.
2016-05-20	Merge branch 'v8.5'	Pierre-Marie Pédrot

2016-05-08	Removing dead code and unused opens.	Pierre-Marie Pédrot

2016-03-20	Moving Evarutil and Proofview to engine/	Pierre-Marie Pédrot