From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 29 Jul 2005 08:10:41 +0000 (+0000)
Subject: 0. core_notation.ma splitted into coq.moo and core_notation.moo
X-Git-Tag: V_0_7_2~5
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=650e3b3c9ff0b9cafb76a0edf8139a53446937ba;hp=650e3b3c9ff0b9cafb76a0edf8139a53446937ba;p=helm.git

0. core_notation.ma splitted into coq.moo and core_notation.moo
1. 'include "coq.ma"' is now explicitly required to activate the notation of Coq
2. 'include "coq.ma"' added here and there in the tests
3. .ma headers updated
---