coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-02-04	Correct bug in non max local implicit arguments	SimonBoulier
	+ tests in the test-suite for non max local implicit arguments
2020-02-04	Add syntax for non maximally inserted implicit arguments	SimonBoulier

2018-10-04	test-suite: cleaning	Vincent Laporte

2018-03-30	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin

2017-05-31	Fixing a failure to interpret some local implicit arguments in Inductive.	Hugo Herbelin
	For instance, the following was failing to use the implicitness of n: Inductive A (P:forall m {n}, n=m -> Prop) := C : P 0 eq_refl -> A P.
2017-04-09	Fixing several wrong computations of implicit arguments by position	Hugo Herbelin
	in the presence of let-ins.
2013-05-08	Declaration of multiple hypotheses or parameters now share typing	herbelin
	information for inference of implicit arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16487 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-18	Unset Asymmetric Patterns	pboutill
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-22	Correct implementation of discharging of implicit arguments and add new	msozeau
	setting "Set Manual Implicit Arguments" for manual-only implicits. Fix test-suite script. This removes the discharge_info argument of "dynamic" object's rebuild function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11242 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-15	Forgot the test file.	msozeau
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10678 85f007b7-540e-0410-9357-904b9bb8a0f7