aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pattern.ml
diff options
context:
space:
mode:
authorherbelin2009-04-09 12:21:04 +0000
committerherbelin2009-04-09 12:21:04 +0000
commit3588bde12b2b8d531b3b2ffde7e79d32c3acd040 (patch)
tree173dc02b07f6cc9407e5d75763e140d63b5a06ed /pretyping/pattern.ml
parent16ea6252339bed9901fff48b5883f4d471a88e7a (diff)
Turning tauto into a classical tautology prover as soon as classical
logic (file Classical_Prop.v) is loaded. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12077 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pattern.ml')
0 files changed, 0 insertions, 0 deletions