]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/tests/match06.cic.test
ocaml 3.09 transition
[helm.git] / helm / gTopLevel / tests / match06.cic.test
index d7078f0ac0a77d0bedf3ec1098fbfe0fe8ead918..eb134e429a5bf557db2e84c3fe34717d70dac30a 100644 (file)
@@ -1,6 +1,10 @@
 \lambda x:False.
   [\lambda h:False. True]
   match x:False with []
+###### INTERPRETATION NUMBER 1 ######
+### (* disambiguation environment  *)
+alias id False = cic:/Coq/Init/Logic/False.ind#xpointer(1/1)
+alias id True = cic:/Coq/Init/Logic/True.ind#xpointer(1/1)
 ### (* METASENV after disambiguation  *)
 
 ### (* TERM after disambiguation      *)