Skip to content

Commit

Permalink
Fix refine bug
Browse files Browse the repository at this point in the history
  • Loading branch information
Edwin Brady committed Aug 23, 2011
1 parent 21dcadb commit 23d8bc6
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions Ivor/Tactics.lhs
View file
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -360,6 +360,8 @@ names. Let's record which ones...
> mkns (UN a) (UN b) = UN (a++"_"++b) > mkns (UN a) (UN b) = UN (a++"_"++b)
> mkns (MN (a,i)) (UN b) = MN (a++"_"++b, i) > mkns (MN (a,i)) (UN b) = MN (a++"_"++b, i)
> mkns (MN (a,i)) (MN (b,j)) = MN (a++"_"++b, i) > mkns (MN (a,i)) (MN (b,j)) = MN (a++"_"++b, i)
> mkns (UN b) (MN (a,i)) = MN (b++"_"++a, i)
> mkns x y = error $ "FAIL: " ++ show (x,y)


> doClaims :: Name -> [((Name, TT Name), Maybe (TT Name))] -> Tactic > doClaims :: Name -> [((Name, TT Name), Maybe (TT Name))] -> Tactic
> doClaims h [] gam env tm = tacret $ tm > doClaims h [] gam env tm = tacret $ tm
Expand Down

0 comments on commit 23d8bc6

Please sign in to comment.