diff --git a/src/TTImp/Elab.idr b/src/TTImp/Elab.idr
index 3d8eb4ab87..1cb87965ed 100644
--- a/src/TTImp/Elab.idr
+++ b/src/TTImp/Elab.idr
@@ -120,7 +120,9 @@ elabTermSub {vars} defining mode opts nest env env' sub tm ty
 
          defs <- get Ctxt
          e <- newRef EST (initEStateSub defining env' sub)
-         let rigc = getRigNeeded mode
+         let rigc = case foldMap (\case OverrideRig x => Just x; _ => Nothing) opts of
+                      Nothing => getRigNeeded mode
+                      Just x  => x
 
          (chktm, chkty) <- check {e} rigc (initElabInfo mode) nest env tm ty
          -- Final retry of constraints and delayed elaborations
diff --git a/src/TTImp/Elab/Check.idr b/src/TTImp/Elab/Check.idr
index 6b4fe3868d..5226aea730 100644
--- a/src/TTImp/Elab/Check.idr
+++ b/src/TTImp/Elab/Check.idr
@@ -49,6 +49,7 @@ data ElabOpt
   | InCase
   | InPartialEval
   | InTrans
+  | OverrideRig RigCount
 
 public export
 Eq ElabOpt where
@@ -56,6 +57,7 @@ Eq ElabOpt where
   InCase == InCase = True
   InPartialEval == InPartialEval = True
   InTrans == InTrans = True
+  OverrideRig x == OverrideRig y = x == y
   _ == _ = False
 
 -- Descriptions of implicit name bindings. They're either just the name,
diff --git a/src/TTImp/ProcessRunElab.idr b/src/TTImp/ProcessRunElab.idr
index 786f20eae7..9ab2e01358 100644
--- a/src/TTImp/ProcessRunElab.idr
+++ b/src/TTImp/ProcessRunElab.idr
@@ -38,6 +38,5 @@ processRunElab eopts nest env fc tm
          unit <- getCon fc defs (builtin "Unit")
          exp <- appCon fc defs n [unit]
 
-         e <- newRef EST $ initEStateSub tidx env SubRefl
-         (stm, _) <- check bot (initElabInfo InExpr) nest env tm $ Just $ gnf env exp
+         stm <- checkTerm tidx InExpr (OverrideRig bot :: eopts) nest env tm (gnf env exp)
          ignore $ elabScript top fc nest env !(nfOpts withAll defs env stm) Nothing