coq - The formal proof system

Age	Commit message (Collapse)	Author
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

2017-09-07	Communicate the backtrace through the monad.	Pierre-Marie Pédrot

2017-09-06	Fix coq/ltac2#23: Int.compare should not be uniformly 0.	Pierre-Marie Pédrot
	Stupid typo.
2017-09-06	Using higher-order representation for closures.	Pierre-Marie Pédrot

2017-09-06	Parameterizing over parameters in ML functions from Tac2core.	Pierre-Marie Pédrot

2017-09-06	The interp_app function now takes a closure as an argument.	Pierre-Marie Pédrot

2017-09-06	Moving Tac2ffi before Tac2interp.	Pierre-Marie Pédrot

2017-09-06	Introducing abstract data representations.	Pierre-Marie Pédrot

2017-09-06	Code factorization.	Pierre-Marie Pédrot

2017-09-05	Refine does not evar-normalizes the goal preemptively.	Pierre-Marie Pédrot

2017-09-05	Binding the firstorder tactic.	Pierre-Marie Pédrot

2017-09-05	Binding move and intro.	Pierre-Marie Pédrot

2017-09-05	Introducing quotations for move locations.	Pierre-Marie Pédrot

2017-09-05	Binding the inversion family of tactics.	Pierre-Marie Pédrot

2017-09-05	Typeclasses_eauto strategy is now optional.	Pierre-Marie Pédrot

2017-09-05	Quotations for auto-related tactics.	Pierre-Marie Pédrot

2017-09-05	More static invariants for typeclass_eauto.	Pierre-Marie Pédrot

2017-09-05	ML bindings of auto-related tactics.	Pierre-Marie Pédrot

2017-09-04	More notations for primitive tactics.	Pierre-Marie Pédrot

2017-09-04	More precise error messages for scope failure.	Pierre-Marie Pédrot

2017-09-04	Implementing the non-strict mode.	Pierre-Marie Pédrot

2017-09-04	Better backtraces for a few datatypes.	Pierre-Marie Pédrot

2017-09-04	Quick-and-dirty backtrace mechanism for the interpreter.	Pierre-Marie Pédrot

2017-09-04	Closures now wear the constant they originated from.	Pierre-Marie Pédrot

2017-09-04	Fix coq/ltac2#17: Assertion failed. on only shelved goals remaining.	Pierre-Marie Pédrot
	We check that the goal tactic is focussed before calling enter_one.
2017-09-04	Implementing lazy matching over terms.	Pierre-Marie Pédrot

2017-09-04	Proper anomalies for missing registered primitives.	Pierre-Marie Pédrot