coq - The formal proof system

Age	Commit message (Collapse)	Author
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.
2017-08-29	Pass Ltac2 variables in a dedicated environment for generic arguments.	Pierre-Marie Pédrot
	This is a way to hack around the fact that various interpretation functions rely wrongly on the values of the environment to do nasty tricks. Typically, the interpretation of terms is broken, as it will fail when there is a bound variable with the same name as a hypothesis, instead of producing the hypothesis itself.
2017-08-29	Removing dead code for handling of array litterals.	Pierre-Marie Pédrot

2017-08-29	Factorizing code for declaration of primitive tactics.	Pierre-Marie Pédrot

2017-08-29	Implementing Ltac2 antiquotations in constr syntax.	Pierre-Marie Pédrot

2017-08-29	Binding an unsafe substitution function.	Pierre-Marie Pédrot

2017-08-29	Binding primitives to generate fresh variables.	Pierre-Marie Pédrot

2017-08-28	Fix coq/ltac2#6: Expected and actual types are flipped.	Pierre-Marie Pédrot

2017-08-27	Do not reuse the Val.t type in toplevel values.	Pierre-Marie Pédrot

2017-08-27	Ensure no confusion with unit in rigid variables.	Pierre-Marie Pédrot

2017-08-27	Proper handling of rigid variables in subtyping.	Pierre-Marie Pédrot

2017-08-27	Introducing rebindable toplevel definitions.	Pierre-Marie Pédrot

2017-08-26	Allowing calls to Ltac2 inside Ltac1.	Pierre-Marie Pédrot

2017-08-26	Allowing to insert calls to Ltac1 references in Ltac2.	Pierre-Marie Pédrot

2017-08-25	Introducing a distinct bindings scope.	Pierre-Marie Pédrot

2017-08-25	Renaming the bindings scope into with_bindings.	Pierre-Marie Pédrot

2017-08-25	Do not return STRING scopes in the tuple produced by "seq" scopes.	Pierre-Marie Pédrot

2017-08-25	More bindings to primitive tactics.	Pierre-Marie Pédrot

2017-08-25	Respect the default goal selector in toplevel invocations.	Pierre-Marie Pédrot

2017-08-25	Parse specifically idents as destruction arguments.	Pierre-Marie Pédrot
	This is for backward compatibility.