Commit 0b3723bd authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Successful build (on Fri 17 May 2019 09:54:43 PM CEST)

parent bd8c39ad
......@@ -173,7 +173,7 @@ instance (Show a,IsCapriconString str,MonadReader (Env str (NormalTerm str a)) m
let newEnv =
let (ch,ct) = splitAt i ctx
in zipWith (\j -> second $ second $ substn (raiseRefs (negate (1+j)) x) (i-j-1)) [0..] ch+drop 1 ct
dx = normalDepth nx ; dm = length ctx
dx = length cx ; dm = length ctx
return (liftUpdate dm dx ux cx (substn x i),newEnv)
insertHypBefore bef h nth = do
NormalTerm (NormalType uth cth _) th <- pullTerm bef nth
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment