diff options
Diffstat (limited to 'dev/ocamldoc')
| -rw-r--r-- | dev/ocamldoc/docintro | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ocamldoc/docintro b/dev/ocamldoc/docintro index 20c3de5ef..33d20fc81 100644 --- a/dev/ocamldoc/docintro +++ b/dev/ocamldoc/docintro @@ -30,7 +30,7 @@ describes the Coq library, which is made of two parts: describes the translation from Coq context-dependent front abstract syntax of terms {v constr_expr v} to and from the -context-free, untyped, globalized form of constructions {v rawconstr v}.} +context-free, untyped, globalized form of constructions {v glob_constr v}.} {- Parsers and printers : parsing describes the implementation of the Coq parsers and printers.} |