coq - The formal proof system

Age	Commit message (Collapse)	Author
2014-04-28	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin
	one_inductive_body so that when eta-expanding at "match" printing time we know if a let is part of the expected signature or part of the body. This is an easy fix for bugs like #3293. Another fix could be to enforce, as an invariant, or better syntactically, that "match"/"Case"'s have the body of their branches expanded.
2013-11-24	Tweaking arity & allocation of some basic functions.	Pierre-Marie Pédrot

2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵	xclerc
	with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-29	Removed many calls to OCaml generic equality. This was done by	ppedrot
	writing our own comparison functions, and enforcing monomorphization in many places. This should be more efficient, btw. Still a work in progress. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15932 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17	Using weak tables instead of plain hash tables while hashconsing.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15899 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-26	Reusing the Hashset data structure in Hashcons. Hopefully, this should	ppedrot
	not disrupt anything... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15836 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-26	Cleaning, renaming obscure functions and documenting in Hashcons.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15834 85f007b7-540e-0410-9357-904b9bb8a0f7