Merge branch 'master' of http://git.megacz.com/coq-hetmet

Conflicts:
	src/Extraction-prefix.hs

diff --cc src/Extraction-prefix.hs
index ea7cabf,56322c9..fbe22cb
--- 1/src/Extraction-prefix.hs
--- 2/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@@ -51,11 -58,9 +51,8 @@@ cmpAlts (a1,_,_) (a2,_,_)         = Dat
  sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)]
  sortAlts x = Data.List.sortBy (\a b -> if a `CoreSyn.ltAlt` b then Data.Ord.LT else Data.Ord.GT) x
  
 --- to do: this could be moved into Coq
  coreVarToWeakVar :: Var.Var -> WeakVar
  coreVarToWeakVar v | Id.isId     v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v))))
-  where
-   errOrFail (OK x)    = x
-   errOrFail (Error s) = Prelude.error s
  coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v)))
  coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME") 
                                                               (Prelude.error "FIXME") (Prelude.error "FIXME"))