coq - The formal proof system

Age	Commit message (Expand)	Author
2012-03-14	Second step of integration of Program:	msozeau
2012-03-14	Remove support for "abstract typing constraints" that requires unicity of sol...	msozeau
2012-03-13	A bit of cleaning: unifying push_rels and push_rel_context.	herbelin
2012-03-13	Fixing vm_compute bug #2729 (function used to decompose constructors	herbelin
2012-03-12	Univ: avoid recording dummy universe constraints u<=u or u=u	letouzey
2012-03-02	Glob_term.predicate_pattern: No number of parameters with letins.	pboutill
2012-03-02	"Let in" in pattern hell, one more iteration	pboutill
2012-03-02	Noise for nothing	pboutill
2012-03-01	Univ: a univ_depends function to avoid a hack in Inductiveops	letouzey
2012-03-01	Univ: a better Constraint.compare	letouzey
2012-03-01	Corrects the erroneous error message when trying to unfocus a fully	aspiwack
2012-03-01	Removed a superfluous function in proof.mli. Preparing for incoming	aspiwack
2012-03-01	New version of recdef :	jforest
2012-03-01	various corrections in invfun due to a modification in induction	jforest
2012-02-29	Univ: a faster is_leq test used when possible	letouzey
2012-02-29	correcting a little bug in invfun.ml	jforest
2012-02-29	correction of bug 2457	jforest
2012-02-29	Fix compilation of Constrintern...	pboutill
2012-02-29	RefMan update about match syntax.	pboutill
2012-02-29	In the syntax of pattern matching, the arguments of the inductive in the "in"	pboutill
2012-02-29	In the syntax of pattern matching, "in" clauses are patterns.	pboutill
2012-02-29	Vector: missing injection lemmas and better impossible branches	pboutill
2012-02-29	Bug 2703: send stdout dump to coqide when an error occurs.	pboutill
2012-02-29	Coq_makefile: Add of extra options by default	pboutill
2012-02-27	Univ: correct compare_neq (fix #2703)	letouzey
2012-02-23	Implement the substitution function for global options. Fixes anomaly in ssre...	msozeau
2012-02-22	Ide: sentences found by find_phrase_starting_at should be nonempty (fix #2683)	letouzey
2012-02-20	Use a heuristic to not simplify equality hypotheses remaining after dependent...	msozeau
2012-02-20	- changing minimal version for OCaml: Coq uses Filename.dirsep that is availa...	notin
2012-02-20	Correct application of head reduction.	msozeau
2012-02-18	Document the [unify] tactic.	msozeau
2012-02-16	Fix handling of space after "Notation" or "where", add missing keywords.	msozeau
2012-02-15	Avoid retrying uncessarily to prove independent remaining obligations in Prog...	msozeau
2012-02-15	Avoid unnecessary normalizations w.r.t. evars in Program.	msozeau
2012-02-15	Fix in evarutil: add a conversion problem for ?x ts = ?x us only if ts and us...	msozeau
2012-02-14	In [reflexivity], [symmetry] etc, use the type found by looking at the relati...	msozeau
2012-02-14	- Fix dependency computation in eterm to not consider filtered variables.	msozeau
2012-02-14	Arguments supports extra notation scopes	gareuselesinge
2012-02-07	Additional comment on Focus Conditions.	aspiwack
2012-02-07	Documentation for Grab Existential Variables.	aspiwack
2012-02-07	A "Grab Existential Variables" to transform the unresolved evars at the end o...	aspiwack
2012-02-07	Typo in comments.	aspiwack
2012-02-03	correcting inversion in list of generated tcc of Function	letouzey
2012-02-02	More information returned by coqtop about its internal state. Hopefully we'll...	ppedrot
2012-02-01	Fix unblocking code in dependent destruction due to zeta being used in unfold...	msozeau
2012-02-01	Corrected a careless cut-and-paste in Gallina description which dated back to...	ppedrot
2012-02-01	Debugger vs tracer: Two different behaviors wrt printing: The debugger	herbelin
2012-02-01	Improved synchronisation of stdlib index page with current library state.	herbelin
2012-01-31	Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...	msozeau
2012-01-31	index-list.html.template: add missing files	pboutill