coq - The formal proof system

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

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

2017-09-03	Allowing complex types in ML objects.	Pierre-Marie Pédrot

2017-09-03	Fix coq/ltac2#16: Passing Ltac2 variables to Ltac1 via $ results in anomalies.	Pierre-Marie Pédrot

2017-09-02	Fix coq/ltac2#12: Error should name which match cases are unhandled.	Pierre-Marie Pédrot

2017-09-02	Fix coq/ltac2#15: Ltac2 scope cannot be disabled after it is required.	Pierre-Marie Pédrot
	Instead of setting globally the option, we add a hook to set it in the init object of the plugin.
2017-09-01	Ensuring the Ltac definitions have lowercase names.	Pierre-Marie Pédrot

2017-08-31	Properly handling internal errors from Coq.	Pierre-Marie Pédrot

2017-08-31	Expand the primitive functions on terms.	Pierre-Marie Pédrot

2017-08-31	Fix coq/ltac2#10: Antiquotation syntax breaks when backtracking across ↵	Pierre-Marie Pédrot
	`Require`.
2017-08-31	Fix coq/ltac2#3: Constructor expects n arguments should name which ↵	Pierre-Marie Pédrot
	constructor it is.
2017-08-30	Binding reduction functions acting on terms.	Pierre-Marie Pédrot

2017-08-29	Fix printing of Ltac2 in quotations.	Pierre-Marie Pédrot

2017-08-29	Fixing printing of tactic expressions.	Pierre-Marie Pédrot

2017-08-29	Centralizing tag declarations.	Pierre-Marie Pédrot

2017-08-29	Rolling our own generic arguments.	Pierre-Marie Pédrot

2017-08-29	Rolling our own dynamic types for Ltac2.	Pierre-Marie Pédrot
	This prevents careless confusions with generic arguments from Coq.