diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-25 21:14:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-11 18:53:35 +0200 |
| commit | 0dc203ee2983594fa064a84739d87f177636f18a (patch) | |
| tree | 21ac9c1a6006260b6a64cfc0ba50b6b13879ac14 /doc | |
| parent | 88decfce9eb63c9659e692b41376de7b608e0d43 (diff) | |
Doc: Some quotes missing in file tactics.rst.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 3278bfd47..064a540ec 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -632,7 +632,7 @@ context. The new subgoal is :g:`U`. If the goal is a non-dependent product :g:`T`:math:`\rightarrow`:g:`U`, then it puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` or -:g:`Prop`) or Xn:T (if the type of :g:`T` is :g:`Type`). The optional index +:g:`Prop`) or :g:`Xn:T` (if the type of :g:`T` is :g:`Type`). The optional index ``n`` is such that ``Hn`` or ``Xn`` is a fresh identifier. In both cases, the new subgoal is :g:`U`. |