coq - The formal proof system

Age	Commit message (Expand)	Author
2014-09-14	Rewrite.apply_strategy uses the same return type as strategies.	Pierre-Marie Pédrot
2014-09-14	Proper type for rewrite strategy results.	Pierre-Marie Pédrot
2014-09-13	Prepare goal name printing but no not print them at the current time.	Hugo Herbelin
2014-09-13	Using "Evd.restrict" in tactic clear so as to keep evar names.	Hugo Herbelin
2014-09-13	Exporting apply_subfilter from Evd.ml.	Hugo Herbelin
2014-09-13	Retroknowledge arguments are made VERNAC ARGUMENTS.	Pierre-Marie Pédrot
2014-09-13	Fixing synchronization of evar names table when merging evar_map.	Hugo Herbelin
2014-09-13	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin
2014-09-13	Checking typability of evar instances. Using ";" to separate bindings	Hugo Herbelin
2014-09-13	Fixing injection bug #3616 on sigma-types.	Hugo Herbelin
2014-09-12	While we don't have a clean alternative to Clenvtac, add a primitive	Matthieu Sozeau
2014-09-12	Fix base_include due to change in argument order of env and evar_map	Matthieu Sozeau
2014-09-12	An old typo which was preventing example #3537 to work the same as it	Hugo Herbelin
2014-09-12	Add syntax [id]: to apply tactic to goal named id.	Hugo Herbelin
2014-09-12	Use evar name to print goal.	Hugo Herbelin
2014-09-12	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin
2014-09-12	Parsing evar instances.	Hugo Herbelin
2014-09-12	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin
2014-09-12	No plural for only one non existing focused goal.	Hugo Herbelin
2014-09-12	Fix source of initial goal.	Hugo Herbelin
2014-09-12	Commit 682aa67cc80 about enforcing that apply does not create new	Hugo Herbelin
2014-09-12	Discontinued xml plugin: improve the README.	Arnaud Spiwack
2014-09-12	Replace the list of argument in tacexpr with a single row argument.	Arnaud Spiwack
2014-09-11	Oopps.. fixed the .ml not the .ml4	Matthieu Sozeau
2014-09-11	Use an AST for strategy names.	Matthieu Sozeau
2014-09-11	Fix test-suite files, and move some opened to closed.	Matthieu Sozeau
2014-09-11	Add a flag for restricting resolution of typeclasses to	Matthieu Sozeau
2014-09-11	Keeping a sub-optimal behavior of intros_possibly_replacing for compatibility...	Hugo Herbelin
2014-09-11	Other bugs with "inversion as" (collision between user-provided names and gen...	Hugo Herbelin
2014-09-11	Fix bug #3594: eta for constructors and functions at the same time which	Matthieu Sozeau
2014-09-11	Fix bug #3596, wrong treatment of projections in compute_constelim_direct.	Matthieu Sozeau
2014-09-11	Fix bug #3505.	Matthieu Sozeau
2014-09-11	Fixing bug #3605.	Pierre-Marie Pédrot
2014-09-11	Removing remaining documentation of the XML plugin.	Pierre-Marie Pédrot
2014-09-10	A step towards better differentiating when w_unify is used for subterm	Hugo Herbelin
2014-09-10	Parsing and printing of primitive projections, fix buggy behavior when	Matthieu Sozeau
2014-09-10	Fix generation of inductive elimination principle for primitive records.	Matthieu Sozeau
2014-09-10	Fix categorization of recursive inductives.	Matthieu Sozeau
2014-09-10	Fixing localisation of tactic errors (my mistake in himsg.ml essentially).	Hugo Herbelin
2014-09-10	More small bugs in intros_replacing.	Hugo Herbelin
2014-09-10	Fixing inversion after having fixed intros_replacing	Hugo Herbelin
2014-09-10	Example for apply and evars.	Hugo Herbelin
2014-09-10	Removing "eqn:" for "induction" in reference manual.	Hugo Herbelin
2014-09-10	VernacExtend does not dispatch on type anymore.	Pierre-Marie Pédrot
2014-09-09	- Fix printing and parsing of primitive projections, including the Set	Matthieu Sozeau
2014-09-09	Merge remote-tracking branch 'jason/win32-improvements' into trunk	Enrico Tassi
2014-09-09	Bump CoqSDK revision number	Jason Gross
2014-09-09	Add a VERBOSE flag to make-sdk-win32	Jason Gross
2014-09-09	Minor code style cleanup in make-sdk-win32	Jason Gross
2014-09-09	Support 64-bit cygwin	Jason Gross