Coq main source components (in link order) ------------------------------------------ clib : Basic files in lib/, such as util.ml lib : Other files in lib/ kernel library pretyping interp proofs printing parsing tactics toplevel highparsing : Files in parsing/ that cannot be linked too early. Contains the grammar rules g_*.ml4 Special components ------------------ intf : Contains mli-only interfaces, many of them providing a.s.t. used for dialog bewteen coq components. Ex: Constrexpr.constr_expr produced by parsing and transformed by interp. grammar : Camlp4 syntax extensions. The file grammar/grammar.cma is used to pre-process .ml4 files containing EXTEND constructions, either TACTIC EXTEND, ARGUMENTS EXTEND or VERNAC ... EXTEND. This grammar.cma incorporates many files from other directories (mainly parsing/), plus some specific files in grammar/. The other syntax extension grammar/q_constr.cmo is a addition to grammar.cma with a constr PATTERN quotation. Hierarchy of A.S.T. ------------------- *** Terms *** ... ... | /\ parsing | | printing | | V | Constrexpr.constr_expr | /\ constrintern | | constrextern (in interp) | | (in interp) globalization | | V | Glob_term.glob_constr | /\ pretyping | | detyping | | (in pretyping) V | Term.constr | /\ safe_typing | | (validation | | by kernel) |______| *** Patterns *** | | parsing V constr_pattern_expr = constr_expr | | Constrintern.interp_constr_pattern (in interp) | reverse way in Constrextern V Pattern.constr_pattern | ---> used for instance by Matching.matches (in pretyping) *** Notations *** Notation_term.notation_constr Conversion from/to glob_constr in Notation_ops TODO... *** Tactics *** | | parsing V Tacexpr.raw_tactic_expr | | Tacinterp.intern_pure_tactic (?) V Tacexpr.glob_tactic_expr | | Tacinterp.eval_tactic (?) V Proof_type.tactic TODO: check with Hugo *** Vernac expressions *** Vernacexpr.vernac_expr, produced by parsing, used in Vernacentries and Vernac