@@ -1325,96 +1325,105 @@ instance Binary PTerm where
13251325 PRef x1 x2 -> do putWord8 1
13261326 put x1
13271327 put x2
1328− PLam x1 x2 x3 -> do putWord8 2
1328+ PInferRef x1 x2 -> do putWord8 2
1329+ put x1
1330+ put x2
1331+ PPatvar x1 x2 -> do putWord8 3
1332+ put x1
1333+ put x2
1334+ PLam x1 x2 x3 -> do putWord8 4
13291335 put x1
13301336 put x2
13311337 put x3
1332− PPi x1 x2 x3 x4 -> do putWord8 3
1338+ PPi x1 x2 x3 x4 -> do putWord8 5
13331339 put x1
13341340 put x2
13351341 put x3
13361342 put x4
1337− PLet x1 x2 x3 x4 -> do putWord8 4
1343+ PLet x1 x2 x3 x4 -> do putWord8 6
13381344 put x1
13391345 put x2
13401346 put x3
13411347 put x4
1342− PTyped x1 x2 -> do putWord8 5
1348+ PTyped x1 x2 -> do putWord8 7
13431349 put x1
13441350 put x2
1345− PApp x1 x2 x3 -> do putWord8 6
1351+ PApp x1 x2 x3 -> do putWord8 8
13461352 put x1
13471353 put x2
13481354 put x3
1349− PCase x1 x2 x3 -> do putWord8 7
1355+ PAppBind x1 x2 x3 -> do putWord8 9
1356+ put x1
1357+ put x2
1358+ put x3
1359+ PMatchApp x1 x2 -> do putWord8 10
1360+ put x1
1361+ put x2
1362+ PCase x1 x2 x3 -> do putWord8 11
13501363 put x1
13511364 put x2
13521365 put x3
1353− PTrue x1 -> do putWord8 8
1366+ PTrue x1 -> do putWord8 12
13541367 put x1
1355− PFalse x1 -> do putWord8 9
1368+ PFalse x1 -> do putWord8 13
13561369 put x1
1357− PRefl x1 x2 -> do putWord8 10
1370+ PRefl x1 x2 -> do putWord8 14
13581371 put x1
13591372 put x2
1360− PResolveTC x1 -> do putWord8 11
1373+ PResolveTC x1 -> do putWord8 15
13611374 put x1
1362− PEq x1 x2 x3 -> do putWord8 12
1375+ PEq x1 x2 x3 -> do putWord8 16
13631376 put x1
13641377 put x2
13651378 put x3
1366− PPair x1 x2 x3 -> do putWord8 13
1379+ PRewrite x1 x2 x3 x4 -> do putWord8 17
1380+ put x1
1381+ put x2
1382+ put x3
1383+ put x4
1384+ PPair x1 x2 x3 -> do putWord8 18
13671385 put x1
13681386 put x2
13691387 put x3
1370− PDPair x1 x2 x3 x4 -> do putWord8 14
1388+ PDPair x1 x2 x3 x4 -> do putWord8 19
13711389 put x1
13721390 put x2
13731391 put x3
13741392 put x4
1375− PAlternative x1 x2 -> do putWord8 15
1393+ PAlternative x1 x2 -> do putWord8 20
13761394 put x1
13771395 put x2
1378− PHidden x1 -> do putWord8 16
1396+ PHidden x1 -> do putWord8 21
13791397 put x1
1380− PType -> putWord8 17
1381− PConstant x1 -> do putWord8 18
1398+ PType -> putWord8 22
1399+ PGoal x1 x2 x3 x4 -> do putWord8 23
1400+ put x1
1401+ put x2
1402+ put x3
1403+ put x4
1404+ PConstant x1 -> do putWord8 24
13821405 put x1
1383− Placeholder -> putWord8 19
1384− PDoBlock x1 -> do putWord8 20
1406+ Placeholder -> putWord8 25
1407+ PDoBlock x1 -> do putWord8 26
13851408 put x1
1386− PIdiom x1 x2 -> do putWord8 21
1409+ PIdiom x1 x2 -> do putWord8 27
13871410 put x1
13881411 put x2
1389− PReturn x1 -> do putWord8 22
1412+ PReturn x1 -> do putWord8 28
13901413 put x1
1391− PMetavar x1 -> do putWord8 23
1414+ PMetavar x1 -> do putWord8 29
13921415 put x1
1393− PProof x1 -> do putWord8 24
1416+ PProof x1 -> do putWord8 30
13941417 put x1
1395− PTactics x1 -> do putWord8 25
1418+ PTactics x1 -> do putWord8 31
13961419 put x1
1397− PImpossible -> putWord8 27
1398− PPatvar x1 x2 -> do putWord8 28
1399− put x1
1400− put x2
1401− PInferRef x1 x2 -> do putWord8 29
1420+ PImpossible -> putWord8 33
1421+ PCoerced x1 -> do putWord8 34
1422+ put x1
1423+ PUnifyLog x1 -> do putWord8 35
1424+ put x1
1425+ PNoImplicits x1 -> do putWord8 36
14021426 put x1
1403− put x2
1404− PRewrite x1 x2 x3 x4 -> do putWord8 30
1405− put x1
1406− put x2
1407− put x3
1408− put x4
1409− PGoal x1 x2 x3 x4 -> do putWord8 31
1410− put x1
1411− put x2
1412− put x3
1413− put x4
1414− PAppBind x1 x2 x3 -> do putWord8 32
1415− put x1
1416− put x2
1417− put x3
14181427 get
14191428 = do i <- getWord8
14201429 case i of
@@ -1424,97 +1433,106 @@ instance Binary PTerm where
14241433 x2 <- get
14251434 return (PRef x1 x2)
14261435 2 -> do x1 <- get
1436+ x2 <- get
1437+ return (PInferRef x1 x2)
1438+ 3 -> do x1 <- get
1439+ x2 <- get
1440+ return (PPatvar x1 x2)
1441+ 4 -> do x1 <- get
14271442 x2 <- get
14281443 x3 <- get
14291444 return (PLam x1 x2 x3)
1430− 3 -> do x1 <- get
1445+ 5 -> do x1 <- get
14311446 x2 <- get
14321447 x3 <- get
14331448 x4 <- get
14341449 return (PPi x1 x2 x3 x4)
1435− 4 -> do x1 <- get
1450+ 6 -> do x1 <- get
14361451 x2 <- get
14371452 x3 <- get
14381453 x4 <- get
14391454 return (PLet x1 x2 x3 x4)
1440− 5 -> do x1 <- get
1455+ 7 -> do x1 <- get
14411456 x2 <- get
14421457 return (PTyped x1 x2)
1443− 6 -> do x1 <- get
1458+ 8 -> do x1 <- get
14441459 x2 <- get
14451460 x3 <- get
14461461 return (PApp x1 x2 x3)
1447− 7 -> do x1 <- get
1462+ 9 -> do x1 <- get
14481463 x2 <- get
14491464 x3 <- get
1450− return (PCase x1 x2 x3)
1451− 8 -> do x1 <- get
1452− return (PTrue x1)
1453− 9 -> do x1 <- get
1454− return (PFalse x1)
1465+ return (PAppBind x1 x2 x3)
14551466 10 -> do x1 <- get
14561467 x2 <- get
1457− return (PRefl x1 x2)
1468+ return (PMatchApp x1 x2)
14581469 11 -> do x1 <- get
1459− return (PResolveTC x1)
1470+ x2 <- get
1471+ x3 <- get
1472+ return (PCase x1 x2 x3)
14601473 12 -> do x1 <- get
1474+ return (PTrue x1)
1475+ 13 -> do x1 <- get
1476+ return (PFalse x1)
1477+ 14 -> do x1 <- get
1478+ x2 <- get
1479+ return (PRefl x1 x2)
1480+ 15 -> do x1 <- get
1481+ return (PResolveTC x1)
1482+ 16 -> do x1 <- get
14611483 x2 <- get
14621484 x3 <- get
14631485 return (PEq x1 x2 x3)
1464− 13 -> do x1 <- get
1486+ 17 -> do x1 <- get
1487+ x2 <- get
1488+ x3 <- get
1489+ x4 <- get
1490+ return (PRewrite x1 x2 x3 x4)
1491+ 18 -> do x1 <- get
14651492 x2 <- get
14661493 x3 <- get
14671494 return (PPair x1 x2 x3)
1468− 14 -> do x1 <- get
1495+ 19 -> do x1 <- get
14691496 x2 <- get
14701497 x3 <- get
14711498 x4 <- get
14721499 return (PDPair x1 x2 x3 x4)
1473− 15 -> do x1 <- get
1500+ 20 -> do x1 <- get
14741501 x2 <- get
14751502 return (PAlternative x1 x2)
1476− 16 -> do x1 <- get
1503+ 21 -> do x1 <- get
14771504 return (PHidden x1)
1478− 17 -> return PType
1479− 18 -> do x1 <- get
1505+ 22 -> return PType
1506+ 23 -> do x1 <- get
1507+ x2 <- get
1508+ x3 <- get
1509+ x4 <- get
1510+ return (PGoal x1 x2 x3 x4)
1511+ 24 -> do x1 <- get
14801512 return (PConstant x1)
1481− 19 -> return Placeholder
1482− 20 -> do x1 <- get
1513+ 25 -> return Placeholder
1514+ 26 -> do x1 <- get
14831515 return (PDoBlock x1)
1484− 21 -> do x1 <- get
1516+ 27 -> do x1 <- get
14851517 x2 <- get
14861518 return (PIdiom x1 x2)
1487− 22 -> do x1 <- get
1488− return (PReturn x1)
1489− 23 -> do x1 <- get
1490− return (PMetavar x1)
1491− 24 -> do x1 <- get
1492− return (PProof x1)
1493− 25 -> do x1 <- get
1494− return (PTactics x1)
1495− 27 -> return PImpossible
14961519 28 -> do x1 <- get
1497− x2 <- get
1498− return (PPatvar x1 x2)
1520+ return (PReturn x1)
14991521 29 -> do x1 <- get
1500− x2 <- get
1501− return (PInferRef x1 x2)
1522+ return (PMetavar x1)
15021523 30 -> do x1 <- get
1503− x2 <- get
1504− x3 <- get
1505− x4 <- get
1506− return (PRewrite x1 x2 x3 x4)
1524+ return (PProof x1)
15071525 31 -> do x1 <- get
1508− x2 <- get
1509− x3 <- get
1510− x4 <- get
1511− return (PGoal x1 x2 x3 x4)
1512− 32 -> do x1 <- get
1513− x2 <- get
1514− x3 <- get
1515− return (PAppBind x1 x2 x3)
1526+ return (PTactics x1)
1527+ 33 -> return PImpossible
1528+ 34 -> do x1 <- get
1529+ return (PCoerced x1)
1530+ 35 -> do x1 <- get
1531+ return (PUnifyLog x1)
1532+ 36 -> do x1 <- get
1533+ return (PNoImplicits x1)
15161534 _ -> error "Corrupted binary data for PTerm"
1517−
1535+
15181536instance (Binary t) => Binary (PTactic' t) where
15191537 put x
15201538 = case x of