coq - The formal proof system

Age	Commit message (Collapse)	Author
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 README.	Pierre-Marie Pédrot

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

2017-08-28	typos	gallais

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

2017-08-27	Notation for clear.	Pierre-Marie Pédrot

2017-08-27	Fix semantics of the solve tactical.	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	Typos	Hugo Herbelin

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

2017-08-25	Adding more notations for the lulz.	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.
2017-08-25	Lookahead to cheat the constr parser in order to parse "& IDENT".	Pierre-Marie Pédrot

2017-08-25	primproj: fix bug 5245, hnf on proj with simpl never flag.	Matthieu Sozeau

2017-08-24	Don't strip the newline, don't use \r	Jason Gross
	Not sure entirely what it was supposed to do, but stripping the newline erased the following line
2017-08-24	Swap order of "aggregating..." message and travis_fold	Jason Gross
	Now the folded line starts with "Aggregating..." and not with "---------"
2017-08-24	[ci] [gitlab] coq-dpdgraph: Remove allow-failure	Jason Gross

2017-08-24	Only display travis_fold: on travis	Jason Gross

2017-08-24	Fix the semantics of fail, as it should enter the goal.	Pierre-Marie Pédrot

2017-08-24	Documentation about the transition from Ltac1.	Pierre-Marie Pédrot

2017-08-24	Removing dead code about arrays in the AST.	Pierre-Marie Pédrot

2017-08-24	Rely on quoting for lists instead of hardwiring it in the AST.	Pierre-Marie Pédrot

2017-08-24	Program: fix BZ#5683, missing lift when building case predicate	Matthieu Sozeau

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

2017-08-24	Adding a notation scope for global references.	Pierre-Marie Pédrot

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

2017-08-24	Fix typing of reference quotations.	Pierre-Marie Pédrot

2017-08-24	Adding a scope for reduction flags.	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-24	Update .mailmap file.	Guillaume Melquiond

2017-08-23	Update coypright dates on documentation	Matthieu Sozeau

2017-08-23	Fix BZ#5687: Coqtop died badly modal message box from CoqIDE.	Pierre-Marie Pédrot
	We let the user choose the most appropriate action to do if coqtop decides to go berserk.
2017-08-22	use OCaml 4.03-compatible Filename functions	Paul Steckler

2017-08-22	also in Fun1.smartmap, read, write from same array	Paul Steckler

2017-08-22	Prevent warning about DSTROOT being undefined.	Guillaume Melquiond

2017-08-22	Prevent overallocation in Array.map_to_list and remove custom implementation ↵	Guillaume Melquiond
	from Detyping.
2017-08-22	Fix obsolete description of real numerals.	Guillaume Melquiond

2017-08-21	read, write from same array	Paul Steckler

2017-08-21	Ensuring all .v files end with a newline to make "sed -i" work better on them.	Hugo Herbelin