aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-12-23 18:51:13 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-12-23 18:51:13 +0000
commit4dc1e6db7c6742e098b2f710613afd14fdff3987 (patch)
tree26d9e282ba1d1a13317bc9364b240ddbff47e569
parent6f60984128d38d1166000223f369fdeb1c6af1a3 (diff)
Fix diagram in genarg.mli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13745 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--interp/genarg.mli41
1 files 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