coq - The formal proof system

Age	Commit message (Expand)	Author
2016-04-27	Attempt to slightly improve abusive "Collision between bound	Hugo Herbelin
2016-04-11	Removing the ad-hoc tactic_expr type.	Pierre-Marie Pédrot
2016-04-10	Expliciting the fact that the atomic tactic type is self-contained.	Pierre-Marie Pédrot
2016-03-25	Moving type_uconstr to Pretyping.	Pierre-Marie Pédrot
2016-03-06	Moving Ltac traces to Tacexpr and Tacinterp.	Pierre-Marie Pédrot
2016-03-04	Removing the UConstr entry of the tactic_arg AST.	Pierre-Marie Pédrot
2016-02-29	Moving the "move" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot
2016-02-29	Moving the "exists" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot
2016-02-29	Moving the "symmetry" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot
2016-02-29	Moving the "generalize dependent" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot
2016-02-29	Moving the "clearbody" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot
2016-02-29	Moving the "clear" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot
2016-02-29	Moving the "cofix" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot
2016-02-29	Moving the "fix" tactic to TACTIC EXTEND.	Pierre-Marie Pédrot
2016-02-24	Removing the MetaIdArg entry of tactic expressions.	Pierre-Marie Pédrot
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-02	Separation of concern in TacAlias API.	Pierre-Marie Pédrot
2015-12-30	External tactics and notations now accept any tactic argument.	Pierre-Marie Pédrot
2015-12-24	Removing auto from the tactic AST.	Pierre-Marie Pédrot
2015-12-04	Getting rid of the dynamic node of the tactic AST.	Pierre-Marie Pédrot
2015-12-03	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-12-02	Dead code from August 2014 in apply in.	Hugo Herbelin
2015-10-19	Type delayed_open_constr is now monotonic.	Pierre-Marie Pédrot
2015-10-12	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-10-11	Fixing untimely unexpected warning "Collision between bound variables" (#4317).	Hugo Herbelin
2015-07-02	Merge branch 'v8.5' into trunk	Maxime Dénès
2015-06-29	Code documentation of the TACTIC/VERNAC EXTEND macros.	Pierre-Marie Pédrot
2015-06-25	Remove other types not carried by interpretations in `Tacexpr`.	Arnaud Spiwack
2015-06-25	Remove useless `and_short_name` in interpreted level in `Tacexpr`.	Arnaud Spiwack
2015-02-10	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-02-02	Removing dead code.	Pierre-Marie Pédrot
2015-01-21	Embedding the index of the ML tactic entry in the Tacexpr AST.	Pierre-Marie Pédrot
2015-01-12	Update headers.	Maxime Dénès
2014-12-23	A global [gfail] tactic which works like [fail] except that it fails even if ...	Arnaud Spiwack
2014-12-23	Fix compilation error in some configurations.	Arnaud Spiwack
2014-12-19	Add a backtracking version of Ltac's [match].	Arnaud Spiwack
2014-12-12	Add Ltac syntax for the [tclIFCATCH] primitive.	Arnaud Spiwack
2014-11-09	Removing a unused boolean in the TacMove node of tacexpr AST.	Pierre-Marie Pédrot
2014-11-01	Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.	Arnaud Spiwack
2014-10-25	This commit introduces changes in induction and destruct.	Hugo Herbelin
2014-09-24	Using an or_var rather than the hack with loc for coding a pure ident	Hugo Herbelin
2014-09-12	Replace the list of argument in tacexpr with a single row argument.	Arnaud Spiwack
2014-09-08	Removing the XML plugin.	Pierre-Marie Pédrot
2014-09-02	Removing [revert] tactic from the AST.	Pierre-Marie Pédrot
2014-09-01	Removing the 'inductive' parameter from tacexpr AST.	Pierre-Marie Pédrot
2014-09-01	Moving the decompose tactic out of the AST.	Pierre-Marie Pédrot
2014-08-18	Lazy interpretation of patterns so that expressions such as "intros H H'/H"	Hugo Herbelin
2014-08-18	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin
2014-08-18	Reorganisation of intropattern code	Hugo Herbelin