From 4dc1e6db7c6742e098b2f710613afd14fdff3987 Mon Sep 17 00:00:00 2001
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 23 Dec 2010 18:51:13 +0000
Subject: Fix diagram in genarg.mli

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13745 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/genarg.mli | 41 +++++++++++++++++++++--------------------
 1 file changed, 21 insertions(+), 20 deletions(-)

diff --git a/interp/genarg.mli b/interp/genarg.mli
index 3c825212f..08839698a 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -49,28 +49,29 @@ and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list
 val pr_intro_pattern : intro_pattern_expr located -> Pp.std_ppcmds
 val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
 
-(** The route of a generic argument, from parsing to evaluation
+(** The route of a generic argument, from parsing to evaluation.
+In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.
 
 {% \begin{%}verbatim{% }%}
-             parsing        in_raw                              out_raw
-   char stream ----> glob_type ----> constr_expr generic_argument --------|
-                          encapsulation                         decaps  |
-                                                                        |
-                                                                        V
-                                                                     glob_type
-                                                                        |
-                                                         globalization  |
-                                                                        V
-                                                                    glob_type
-                                                                        |
-                                                                 encaps |
-                                                                in_glob |
-                                                                        V
-                                                     glob_constr generic_argument
-                                                                        |
-        out                          in                        out_glob |
-  type <--- constr generic_argument <---- type <------ glob_type <--------|
-    |  decaps                       encaps      interp           decaps
+             parsing          in_raw                            out_raw
+   char stream ---> raw_object ---> raw_object generic_argument -------+
+                          encapsulation                          decaps|
+                                                                       |
+                                                                       V
+                                                                   raw_object
+                                                                       |
+                                                         globalization |
+                                                                       V
+                                                                   glob_object
+                                                                       |
+                                                                encaps |
+                                                               in_glob |
+                                                                       V
+                                                           glob_object generic_argument
+                                                                       |
+          out                          in                     out_glob |
+  object <--- object generic_argument <--- object <--- glob_object <---+
+    |   decaps                       encaps      interp           decaps
     |
     V
 effective use
-- 
cgit v1.2.3