diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-23 18:51:13 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-23 18:51:13 +0000 |
| commit | 4dc1e6db7c6742e098b2f710613afd14fdff3987 (patch) | |
| tree | 26d9e282ba1d1a13317bc9364b240ddbff47e569 /interp | |
| parent | 6f60984128d38d1166000223f369fdeb1c6af1a3 (diff) | |
Fix diagram in genarg.mli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13745 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/genarg.mli | 41 |
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 |