diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-23 18:50:30 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-23 18:50:30 +0000 |
| commit | fafba6b545c7d0d774bcd79bdbddb8869517aabb (patch) | |
| tree | 1c41d59996f23c4d8d1aefbce96f679533527866 /dev/ocamldoc | |
| parent | cdbbcb3ebb9bed4bba558e6fa4a3b01f3cc18af1 (diff) | |
Prepare change of nomenclature rawconstr -> glob_constr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13742 85f007b7-540e-0410-9357-904b9bb8a0f7
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 3c0e262d4..20c3de5ef 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, raw form of constructions {v rawconstr v}.} +context-free, untyped, globalized form of constructions {v rawconstr v}.} {- Parsers and printers : parsing describes the implementation of the Coq parsers and printers.} |