coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Fixing bug #4269: [Print Assumptions] lies about which axioms a term depends on.	Pierre-Marie Pédrot	2015-09-15
\| \| \| \| \|	This was because the traversal algorithm used canonical names instead of user names, confusing which term was defined and which term was an axiom.
*	Assumptions: more informative print for False axiom (Close: #4054)	Enrico Tassi	2015-06-29
	When an axiom of an empty type is matched in order to inhabit a type, do print that type (as if each use of that axiom was a distinct foo_subproof). E.g. Lemma w : True. Proof. case demon. Qed. Lemma x y : y = 0 /\ True /\ forall w, w = y. Proof. split. case demon. split; [ exact w \| case demon ]. Qed. Print Assumptions x. Prints: Axioms: demon : False used in x to prove: forall w : nat, w = y used in w to prove: True used in x to prove: y = 0