coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-09-04	Implementing the non-strict mode.	Pierre-Marie Pédrot

2017-09-04	Implementing multi-match and simple match over constrs.	Pierre-Marie Pédrot

2017-09-04	Implementing lazy matching over terms.	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-01	Passing an optional message to Tactic_failure.	Pierre-Marie Pédrot

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

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	Implementing Ltac2 antiquotations in constr syntax.	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-25	Adding more notations for the lulz.	Pierre-Marie Pédrot

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

2017-08-24	Adding a notation for the unfold tactic.	Pierre-Marie Pédrot

2017-08-24	Adding notation for the remaining reduction functions.	Pierre-Marie Pédrot

2017-08-24	Introducing a quotation for global references.	Pierre-Marie Pédrot

2017-08-18	Notations for a few reduction functions.	Pierre-Marie Pédrot

2017-08-11	Introducing a syntax for goal dispatch.	Pierre-Marie Pédrot

2017-08-08	Another batch of primitive operations.	Pierre-Marie Pédrot

2017-08-07	Defining several aliases for built-in tactics.	Pierre-Marie Pédrot

2017-08-05	More notations for basic tactics.	Pierre-Marie Pédrot

2017-08-05	Exporting the rewrite tactic.	Pierre-Marie Pédrot

2017-08-04	Adding the induction and destruct tactics.	Pierre-Marie Pédrot

2017-08-04	Introducing notations for destruct and induction arguments.	Pierre-Marie Pédrot

2017-08-02	Inserting enter functions in Ltac1 bindings.	Pierre-Marie Pédrot

2017-08-02	Tentatively implementing apply.	Pierre-Marie Pédrot

2017-08-02	Fix compilation of horrible Ltac2 example.	Pierre-Marie Pédrot

2017-08-02	Properly implementing the notation to easily access hypotheses.	Pierre-Marie Pédrot

2017-08-02	More examples	Pierre-Marie Pédrot

2017-08-02	Adding a few standard notations for Ltac1 tactics.	Pierre-Marie Pédrot

2017-08-02	Better test Makefile.	Pierre-Marie Pédrot

2017-08-01	Don't reuse Coq AST for binding quotations.	Pierre-Marie Pédrot
	This allows antiquotations in binding lists.
2017-08-01	Binding more primitive tactics.	Pierre-Marie Pédrot

2017-08-01	Do not thunk notations preemptively.	Pierre-Marie Pédrot
	One has to rely on the 'thunk' token to produce such thunks.
2017-08-01	Adding new scopes for standard Ltac structures.	Pierre-Marie Pédrot

2017-07-30	Exporting more internals from Coq implementation.	Pierre-Marie Pédrot

2017-07-27	Factorizing code for constructors and tuples.	Pierre-Marie Pédrot

2017-07-27	Using thunks in the horrible Ltac2 example.	Pierre-Marie Pédrot

2017-07-26	Adding an example file	Pierre-Marie Pédrot

2017-07-26	Ensuring that inductive constructors are always capitalized.	Pierre-Marie Pédrot

2017-07-26	Adding a file for testing typing.	Pierre-Marie Pédrot

2017-07-24	Adding a few primitive functions.	Pierre-Marie Pédrot

2017-07-24	Adding quick-n-dirty tests.	Pierre-Marie Pédrot