diff --git a/doc/tactics/clear.rst b/doc/tactics/clear.rst
new file mode 100644
index 000000000..1f60cf499
--- /dev/null
+++ b/doc/tactics/clear.rst
@@ -0,0 +1,60 @@
+========================================================================
+Tactic: `clear`
+========================================================================
+
+The `clear` tactic can be used with any goal to remove hypotheses and
+variables from the context. This is useful to simplify the context by 
+removing assumptions and variables that are no longer needed.
+
+There are two variants of the `clear` tactic: an opt-in variant where
+specific hypotheses and variables are removed, and an opt-out variant 
+where all hypotheses and variables except for the specified ones are removed.
+
+.. admonition:: Syntax
+
+  `clear`
+
+When given no arguments, the `clear` tactic removes all hypotheses and 
+all variables not transitively used in the goal from the context.
+
+.. admonition:: Syntax
+
+  `clear -{idents}`
+
+Here, `{idents}` is a non-empty space separated list of identifiers of
+the hypotheses and variables that should *not* be cleared. The tactic
+removes all hypotheses and variables except for those in the list, and
+those used transitively in the goal *or* in the objects in the list.
+
+.. admonition:: Syntax
+
+  `clear {idents}`
+
+Here, `{idents}` is a non-empty space separated list of identifiers of
+the hypotheses and variables to be cleared. If one of these is transitively
+used in the goal, then it is not cleared and an error is raised.
+
+.. ecproof::
+   :title: Hoare logic example
+
+   lemma L: true.
+   pose x:=false.
+   (*$*) clear x.
+   (* `x` is now unbound *)
+   pose x:=false.
+   pose y:=x.
+   pose z:=y.
+   clear -y. 
+   (* `z` is unbound, but `x` is not, since `y` depends on it *)
+   pose z:=x.
+   clear y.
+   pose y:=z.
+   clear. 
+   (* everything is unbound, since nothing is in the goal *)
+   pose x:=true.
+   pose y:=false.
+   clear. 
+   (* we cannot clear `x` since it is in the goal,
+       but `y` is not used so it becomes unbound *)
+   pose y:= x.
+   abort.