Additional comments about the origins of the code.

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
coq · May 4, 2020 · 9ceec48 · 9ceec48
1 parent 23a0a14
commit 9ceec48
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst
@@ -2,7 +2,7 @@ Primitive objects
 =================
 
 .. _primitive-integers:
-
+.. extracted from gallina extensions chapter
 Primitive Integers
 ------------------
 

diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst
@@ -74,7 +74,7 @@ Inferable subterms
 Expressions often contain redundant pieces of information. Subterms that can be
 automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will
 guess the missing piece of information.
-
+.. extracted from Gallina extensions chapter
 .. _explicit-display-existentials:
 
 Explicit displaying of existential instances for pretty-printing