diff options
| author | sacerdot | 2004-11-16 12:37:40 +0000 |
|---|---|---|
| committer | sacerdot | 2004-11-16 12:37:40 +0000 |
| commit | d6c204c70c3b89b5bda4e7779cc4a20b5fa3f63f (patch) | |
| tree | ed4d954a685588ee55f4d8902eba8a1afc864472 /parsing/printer.ml | |
| parent | 08cb37edb71af0301a72acc834d50f24b0733db5 (diff) | |
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
MOVITATION: in a forthcoming commit the application of a substitution to a
constant will return a constr and not a constant. The application of a
substitution to a kernel_name will return a kernel_name. Thus "constant"
should be use as a kernel name for references that can be delta-expanded.
KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code
that implements "Canonical Structure"s). The ADT is violated once in this
ocaml module. My feeling is that the implementation of "Canonical Structure"s
should be rewritten to avoid this situation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 06a1cc8128..757b61aa1d 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -46,7 +46,7 @@ let dfltpr ast = (str"#GENTERM " ++ print_ast ast);; let global_const_name kn = try pr_global Idset.empty (ConstRef kn) with Not_found -> (* May happen in debug *) - (str ("CONST("^(string_of_kn kn)^")")) + (str ("CONST("^(string_of_con kn)^")")) let global_var_name id = try pr_global Idset.empty (VarRef id) @@ -67,14 +67,14 @@ let global_constr_name ((kn,tyi),i) = let globpr gt = match gt with | Nvar(_,s) -> (pr_id s) | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev))) - | Node(_,"CONST",[Path(_,sl)]) -> - global_const_name (section_path sl) + | Node(_,"CONST",[ConPath(_,sl)]) -> + global_const_name sl | Node(_,"SECVAR",[Nvar(_,s)]) -> global_var_name s | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) -> - global_ind_name (section_path sl, tyi) + global_ind_name (sl, tyi) | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) -> - global_constr_name ((section_path sl, tyi), i) + global_constr_name ((sl, tyi), i) | Dynamic(_,d) -> if (Dyn.tag d) = "constr" then (str"<dynamic [constr]>") else dfltpr gt |