Add missing 'commit' on backtrack

This means we can add things to the main context rather than the staging
context, if the 'branch' is always bracketed with a 'commit'. It doesn't
make a huge difference, but it is at least tidy!

src/Core/Context/Data.idr

@@ -125,8 +125,8 @@ addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons)
     addDataConstructors tag [] gam = pure gam
     addDataConstructors tag (MkCon fc n a ty :: cs) gam
         = do let condef = newDef fc n top vars ty (conVisibility vis) (DCon tag a Nothing)
-             (idx, gam') <- addCtxt n condef gam
              -- Check 'n' is undefined
              Nothing <- lookupCtxtExact n gam
                  | Just gdef => throw (AlreadyDefined fc n)
+             (idx, gam') <- addCtxt n condef gam
              addDataConstructors (tag + 1) cs gam'

src/TTImp/Elab.idr

@@ -249,6 +249,10 @@ checkTermSub defining mode opts nest env env' sub tm ty
                                                    env env' sub
                                                    tm' (Just ty)
                               _ => throw err)
+         case mode of
+              InType => commit -- bracket the 'branch' above
+              _ => pure ()
+
          pure (fst res)
   where
     bindImps' : {vs : _} ->