diff --git a/library/init/lean/elaborator/basic.lean b/library/init/lean/elaborator/basic.lean
index aa48dbbb0d..26d0513c38 100644
--- a/library/init/lean/elaborator/basic.lean
+++ b/library/init/lean/elaborator/basic.lean
@@ -261,6 +261,9 @@ logError stx ("unknown declaration '" ++ toString declName ++ "'")
 def getEnv : Elab Environment :=
 do s ← get; pure s.env
 
+def setEnv (env : Environment) : Elab Unit :=
+modify $ fun s => { env := env, .. s }
+
 def elabTerm (stx : Syntax) : Elab Expr :=
 stx.ifNode
   (fun n => do
diff --git a/library/init/lean/elaborator/command.lean b/library/init/lean/elaborator/command.lean
index 949185cd09..756d5ec99c 100644
--- a/library/init/lean/elaborator/command.lean
+++ b/library/init/lean/elaborator/command.lean
@@ -179,6 +179,13 @@ fun n => do
   let idsStx := n.getArg 1;
   idsStx.mforArgs addUniverse
 
+@[builtinCommandElab «init_quot»] def elabInitQuot : CommandElab :=
+fun _ => do
+  env ← getEnv;
+  match env.addDecl Declaration.quotDecl with
+  | Except.ok env   => setEnv env
+  | Except.error ex => logElabException (ElabException.kernel ex)
+
 /- We just ignore Lean3 notation declaration commands. -/
 @[builtinCommandElab «mixfix»] def elabMixfix : CommandElab := fun _ => pure ()
 @[builtinCommandElab «reserve»] def elabReserve : CommandElab := fun _ => pure ()