coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-10-21	Oops, my bad, didn't expect a merge issue!	Matthieu Sozeau

2016-10-21	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau

2016-10-12	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-09-16	Adding variants enter_one and refine_one which assume that exactly one	Hugo Herbelin
	goal is under focus and which support returning a relevant output.
2016-07-08	Fixing #4906 (regression in printing an error message).	Hugo Herbelin

2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey
	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
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