X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Ftests%2Ffix_betareduction.ma;h=82f0b1cf63e26d1bb498a0dbdaa284e2ad2725cc;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=5056f9e6ecb9f7fd75f0fe778a4111c3a7e4f7ca;hpb=41a53763963ddaa2bb4af0e1b922525bb9fad84e;p=helm.git diff --git a/helm/matita/tests/fix_betareduction.ma b/helm/matita/tests/fix_betareduction.ma index 5056f9e6e..82f0b1cf6 100644 --- a/helm/matita/tests/fix_betareduction.ma +++ b/helm/matita/tests/fix_betareduction.ma @@ -1,3 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/tests/fix_betareduction/". + alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)". alias id "n" = "cic:/Suresnes/BDD/canonicite/Canonicity_BDT/n.con". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".