mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-17 21:11:35 +03:00
Fix haddock parse errors
This commit is contained in:
parent
fd4415803a
commit
f8290af910
@ -1,5 +1,6 @@
|
||||
-- |
|
||||
-- Module : $Header$
|
||||
-- Description : The reference implementation of the Cryptol evaluation semantics.
|
||||
-- Copyright : (c) 2013-2016 Galois, Inc.
|
||||
-- License : BSD3
|
||||
-- Maintainer : cryptol@galois.com
|
||||
@ -8,8 +9,6 @@
|
||||
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
|
||||
-- | The reference implementation of the Cryptol evaluation semantics.
|
||||
|
||||
module Cryptol.Eval.Reference where
|
||||
|
||||
import Control.Applicative (liftA2)
|
||||
|
@ -109,11 +109,11 @@ quickSolverIO ctxt gs =
|
||||
, d
|
||||
])) -- -}
|
||||
|
||||
quickSolver :: Ctxt -> {- ^ Facts we can know -}
|
||||
[Goal] -> {- ^ Need to solve these -}
|
||||
Either Goal (Subst,[Goal])
|
||||
-- ^ Left: contradiciting goals,
|
||||
-- Right: inferred types, unsolved goals.
|
||||
quickSolver :: Ctxt -- ^ Facts we can know
|
||||
-> [Goal] -- ^ Need to solve these
|
||||
-> Either Goal (Subst,[Goal])
|
||||
-- ^ Left: contradicting goals,
|
||||
-- Right: inferred types, unsolved goals.
|
||||
quickSolver ctxt gs0 = go emptySubst [] gs0
|
||||
where
|
||||
go su [] [] = Right (su,[])
|
||||
@ -364,10 +364,9 @@ computeImprovements s gs =
|
||||
, (x,t) : _ <- mapMaybe (improveByDefn ints) gs ->
|
||||
do let su' = singleSubst x t
|
||||
debugLog s ("Improve by definition: " ++ show (pp su'))
|
||||
return (Right su') -}
|
||||
|
||||
-- | otherwise -> return (Right su)
|
||||
|
||||
return (Right su')
|
||||
| otherwise -> return (Right su)
|
||||
-}
|
||||
Nothing ->
|
||||
do bad <- Num.minimizeContradictionSimpDef s
|
||||
(map Num.knownDefined nums)
|
||||
|
Loading…
Reference in New Issue
Block a user