coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-06-18	Fixing a batch of deprecation warnings.	Pierre-Marie Pédrot

2018-05-24	Adapt to fix/cofix changes in Coq (coq/coq#7196)	Emilio Jesus Gallego Arias
	c.f. https://github.com/coq/coq/pull/7196
2018-04-02	[coq] Adapt to coq/coq#6960.	Emilio Jesus Gallego Arias
	Minor, a couple of tactic-related types moved.
2017-11-06	Generalize the use of repr in Tac2stdlib.	Pierre-Marie Pédrot

2017-11-02	Binding the specialize tactic.	Pierre-Marie Pédrot

2017-10-30	Introducing the change tactic.	Pierre-Marie Pédrot

2017-10-07	Remove unused warnings.	Pierre-Marie Pédrot

2017-10-01	Using Ltac2 native closures in some tactic APIs.	Pierre-Marie Pédrot

2017-10-01	Rolling up our own representation of clauses.	Pierre-Marie Pédrot

2017-10-01	Moving ML types used by Ltac2 to their proper interface.	Pierre-Marie Pédrot

2017-09-30	Abstracting away the primitive functions on valexpr datatype.	Pierre-Marie Pédrot

2017-09-26	Adding quotations for the assert family of tactics.	Pierre-Marie Pédrot

2017-09-15	Making Ltac2 representation of data coincide with the ML-side one.	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-07	Communicate the backtrace through the monad.	Pierre-Marie Pédrot

2017-09-06	Using higher-order representation for closures.	Pierre-Marie Pédrot

2017-09-06	The interp_app function now takes a closure as an argument.	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	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	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	Quick-and-dirty backtrace mechanism for the interpreter.	Pierre-Marie Pédrot

2017-08-30	Binding reduction functions acting on terms.	Pierre-Marie Pédrot

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

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

2017-08-24	Use references in reduction tactics.	Pierre-Marie Pédrot
	We dynamically check that the provided references are indeed evaluable ones, instead of ensuring this at internalization time.
2017-08-18	Removing dead code.	Pierre-Marie Pédrot

2017-08-05	Exporting more reduction functions.	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-02	Tentatively implementing apply.	Pierre-Marie Pédrot

2017-08-02	Merging the e/- variants of primitive tactics.	Pierre-Marie Pédrot

2017-08-02	Adding new notations.	Pierre-Marie Pédrot

2017-08-02	Fixup reification of egeneralize.	Pierre-Marie Pédrot

2017-08-01	More primitive tactics.	Pierre-Marie Pédrot

2017-08-01	Introducing the all-mighty intro-patterns.	Pierre-Marie Pédrot

2017-08-01	Binding more primitive tactics.	Pierre-Marie Pédrot

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

2017-07-28	Parameterizing FFI functions for parameterized types.	Pierre-Marie Pédrot

2017-07-28	Moving the Ltac2 FFI to a separate file.	Pierre-Marie Pédrot

2017-07-26	Exporting some basic tactics from Ltac1.	Pierre-Marie Pédrot