helm/gTopLevel/tests/match06.cic.test

   1 \lambda x:False.
   2   [\lambda h:False. True]
   3   match x:False with []
   4 ###### INTERPRETATION NUMBER 1 ######
   5 ### (* disambiguation environment  *)
   6 alias id False = cic:/Coq/Init/Logic/False.ind#xpointer(1/1)
   7 alias id True = cic:/Coq/Init/Logic/True.ind#xpointer(1/1)
   8 ### (* METASENV after disambiguation  *)
   9
  10 ### (* TERM after disambiguation      *)
  11 [x:False]
  12 <[h:False]True>Cases x of
  13 end
  14 ### (* TYPE_OF the disambiguated term *)
  15 (x:False)([h:False]True x)
  16 ### (* REDUCED disambiguated term     *)
  17 [x:False]
  18 <[h:False]True>Cases x of
  19 end