coq - The formal proof system

Age	Commit message (Expand)	Author
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
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
2017-09-09	Fix coq/ltac2#25: Control.case should not be able to catch Control.throw.	Pierre-Marie Pédrot
2017-09-08	Using a dedicated argument for tactic quotations.	Pierre-Marie Pédrot
2017-09-08	Fix coq/ltac2#27: ... is not a particularly helpful printing of an error mess...	Pierre-Marie Pédrot
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
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
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
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
2017-09-03	Introducing a macro for constr matching.	Pierre-Marie Pédrot
2017-09-03	Moving generic arguments to Tac2quote.	Pierre-Marie Pédrot
2017-09-03	Uniform handling of locations in the various AST.	Pierre-Marie Pédrot
2017-09-03	Allowing ML objects to return mere tactic expressions.	Pierre-Marie Pédrot