coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-12-26	adapt to API.mli removal	Enrico Tassi

2017-12-08	Adapt to removal of match_appsubterm.	Théo Zimmermann

2017-11-24	A possible fix after PR#6158 (raw/glob generic printers for ltac values).	Hugo Herbelin
	Can the printers exploit the ability to now take an environment?
2017-11-21	[coq] Adapt to Coq's new functional EXTEND API.	Emilio Jesus Gallego Arias
	See https://github.com/coq/coq/pull/6197
2017-11-06	Generalize the use of repr in Tac2stdlib.	Pierre-Marie Pédrot

2017-11-04	A possible fix after PR#6047 (a generic printer for ltac values).	Hugo Herbelin

2017-11-02	Factorizing entries for patterns with type constraints.	Pierre-Marie Pédrot

2017-11-02	Moving pattern type constraints to pattern AST.	Pierre-Marie Pédrot

2017-11-02	Binding the specialize tactic.	Pierre-Marie Pédrot

2017-10-30	Put notations in level 5 by default.	Pierre-Marie Pédrot

2017-10-30	Fix the semantics of introducing with empty intro patterns.	Pierre-Marie Pédrot

2017-10-30	Introducing the change tactic.	Pierre-Marie Pédrot

2017-10-30	Fix compilation after merge of Ltac_pretype interface.	Pierre-Marie Pédrot

2017-10-27	Better printers for toplevel values.	Pierre-Marie Pédrot

2017-10-27	Adding a command to evaluate Ltac2 expressions.	Pierre-Marie Pédrot

2017-10-27	Fix goal_matching quotation.	Pierre-Marie Pédrot

2017-10-27	Fix relative meaning of Pattern vs. Context in match goal.	Pierre-Marie Pédrot

2017-10-27	Stubs for goal matching: quotation and matching function.	Pierre-Marie Pédrot

2017-10-07	Implementing the Constr.in_context function.	Pierre-Marie Pédrot

2017-10-07	Remove unused warnings.	Pierre-Marie Pédrot

2017-10-07	Fix coq/ltac2#30: Compilation broken since -safe-string PR got merged.	Pierre-Marie Pédrot

2017-10-01	Abstracting away the implementation of value representations.	Pierre-Marie Pédrot

2017-10-01	Using Ltac2 native closures in some tactic APIs.	Pierre-Marie Pédrot

2017-10-01	Rolling up our own representation of clauses.	Pierre-Marie Pédrot

2017-10-01	Moving ML types used by Ltac2 to their proper interface.	Pierre-Marie Pédrot

2017-09-30	Abstracting away the primitive functions on valexpr datatype.	Pierre-Marie Pédrot

2017-09-26	Adding quotations for the assert family of tactics.	Pierre-Marie Pédrot

2017-09-26	Small language of combinators for lookaheads in parsing.	Pierre-Marie Pédrot

2017-09-15	Making Ltac2 representation of data coincide with the ML-side one.	Pierre-Marie Pédrot

2017-09-15	Phantom type for typed closures.	Pierre-Marie Pédrot

2017-09-14	Abstracting away the type of arities and ML tactics.	Pierre-Marie Pédrot

2017-09-14	Moving valexpr definition to Tac2ffi.	Pierre-Marie Pédrot

2017-09-14	Explicit arity for closures.	Pierre-Marie Pédrot

2017-09-14	Introducing the remember tactic.	Pierre-Marie Pédrot

2017-09-14	Binding the pose/set family of tactics.	Pierre-Marie Pédrot

2017-09-14	Use a simpler syntax for generalize grammar.	Pierre-Marie Pédrot
	This removes the use for a quotation.
2017-09-13	Better printing for list literals.	Pierre-Marie Pédrot

2017-09-13	Adding quotations for the generalize tactic.	Pierre-Marie Pédrot

2017-09-09	If backtrace is missing, don't print it.	Pierre-Marie Pédrot

2017-09-09	Update backtraces only when the Ltac2 Backtrace flag is set.	Pierre-Marie Pédrot

2017-09-09	Fix coq/ltac2#26: Ltac1 gives no backtraces.	Pierre-Marie Pédrot

2017-09-09	Fix coq/ltac2#18: Terms should show a backtrace when Set Ltac2 Backtrace is set.	Pierre-Marie Pédrot

2017-09-09	Moving Ltac2 backtraces to the Exninfo mechanism.	Pierre-Marie Pédrot
	I don't know why, but on CoqIDE this triggers a printing of the backtrace twice. This is not reproducible with coqtop.
2017-09-09	Fix coq/ltac2#25: Control.case should not be able to catch Control.throw.	Pierre-Marie Pédrot
	When crossing constr boundaries, we mark exceptions as being fatal not to catch them.
2017-09-08	Using a dedicated argument for tactic quotations.	Pierre-Marie Pédrot
	This prevents having to go through an expensive phase of goal-building, when we can simply type-check the term.
2017-09-08	Fix coq/ltac2#27: ... is not a particularly helpful printing of an error ↵	Pierre-Marie Pédrot
	message.
2017-09-08	Fix coq/ltac2#24: There should be a way to turn an exn into a message.	Pierre-Marie Pédrot

2017-09-08	Fix coq/ltac2#22: Argument to Tactic_failure should be printed.	Pierre-Marie Pédrot
	We implement a printer for toplevel values and use it for exceptions in particular.
2017-09-07	Slightly better printing for anonymous closures.	Pierre-Marie Pédrot

2017-09-07	Fix coq/ltac2#21: Backtraces should print Ltac2 closures.	Pierre-Marie Pédrot