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 +-
 interp/doc.tex                        | 2 +-
 plugins/funind/rawterm_to_relation.ml | 6 +++---
 plugins/funind/rawtermops.mli         | 6 +++---
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/dev/ocamldoc/docintro b/dev/ocamldoc/docintro
index 3c0e262d47..20c3de5efc 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.}
diff --git a/interp/doc.tex b/interp/doc.tex
index 5bd92fbda2..ddf40d6c87 100644
--- a/interp/doc.tex
+++ b/interp/doc.tex
@@ -5,7 +5,7 @@
 \ocwsection \label{interp}
 This chapter describes the translation from \Coq\ context-dependent
 front abstract syntax of terms (\verb=front=) to and from the
-context-free, untyped, raw form of constructions (\verb=rawconstr=).
+context-free, untyped, globalized form of constructions (\verb=rawconstr=).
 
 The modules translating back and forth the front abstract syntax are
 organized as follows.
diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index 5d282a5cb2..f8da96bdfc 100644
--- a/plugins/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
@@ -41,7 +41,7 @@ let compose_raw_context =
 
 
 (*
-   The main part deals with building a list of raw constructor expressions
+   The main part deals with building a list of globalized constructor expressions
    from the rhs of a fixpoint equation.
 *)
 
@@ -879,7 +879,7 @@ let is_res id =
 exception Continue
 (*
    The second phase which reconstruct the real type of the constructor.
-   rebuild the raw constructors expression.
+   rebuild the globalized constructors expression.
    eliminates some meaningless equalities, applies some rewrites......
 *)
 let rec rebuild_cons env nb_args relname args crossed_types depth rt =
@@ -1266,7 +1266,7 @@ let do_build_inductive
       (function result (* (args',concl') *) ->
 	 let rt = compose_raw_context result.context result.value in
 	 let nb_args = List.length funsargs.(i) in
-	 (*  with_full_print (fun rt -> Pp.msgnl (str "raw constr " ++ pr_rawconstr rt)) rt; *)
+	 (*  with_full_print (fun rt -> Pp.msgnl (str "glob constr " ++ pr_rawconstr rt)) rt; *)
 	 fst (
 	   rebuild_cons env_with_graphs nb_args relnames.(i)
 	     []
diff --git a/plugins/funind/rawtermops.mli b/plugins/funind/rawtermops.mli
index 455e7c89b2..4657033869 100644
--- a/plugins/funind/rawtermops.mli
+++ b/plugins/funind/rawtermops.mli
@@ -19,9 +19,9 @@ val pattern_to_term : cases_pattern -> rawconstr
 val mkRRef : Libnames.global_reference -> rawconstr
 val mkRVar : Names.identifier -> rawconstr
 val mkRApp  : rawconstr*(rawconstr list) -> rawconstr
-val mkRLambda : Names.name*rawconstr*rawconstr -> rawconstr
-val mkRProd : Names.name*rawconstr*rawconstr -> rawconstr
-val mkRLetIn : Names.name*rawconstr*rawconstr -> rawconstr
+val mkRLambda : Names.name * rawconstr * rawconstr -> rawconstr
+val mkRProd : Names.name * rawconstr * rawconstr -> rawconstr
+val mkRLetIn : Names.name * rawconstr * rawconstr -> rawconstr
 val mkRCases : rawconstr option * tomatch_tuples * cases_clauses -> rawconstr
 val mkRSort : rawsort -> rawconstr
 val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *)
-- 
cgit v1.2.3