]> matita.cs.unibo.it Git - helm.git/commitdiff
No more garbage in the metasenv.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 5 Feb 2004 18:18:52 +0000 (18:18 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 5 Feb 2004 18:18:52 +0000 (18:18 +0000)
helm/gTopLevel/tests/fix00.cic.test

index f688c4060ffbbe6dfaa869b936e66e20b89110ff..901acd9904558f8fe78e3d7e03af94c5dca2b186 100644 (file)
@@ -7,8 +7,7 @@ let rec fact =
 in
 (fact 4)
 ### (* METASENV after disambiguation  *)
- |- ?2: Type
- |- ?3: ?2[]
+
 ### (* TERM after disambiguation      *)
 [fact:=
 Fix fact {