From fafba6b545c7d0d774bcd79bdbddb8869517aabb Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 23 Dec 2010 18:50:30 +0000 Subject: 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 --- dev/ocamldoc/docintro | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev/ocamldoc') 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.} -- cgit v1.2.3