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

1 files changed, 8 insertions, 0 deletions

diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index ec1e6410e..e1bb51dd7 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -85,6 +85,14 @@ let rec mlexpr_of_ast = function
       let e = expr_list_of_var_list e in
       <:expr< Coqast.Path loc (Libnames.encode_kn (Names.make_dirpath $e$)
                 (Names.id_of_string $str:Names.string_of_id a$)) >> 
+  | Coqast.ConPath (loc, kn) ->
+      let l,a = Libnames.decode_con kn in
+      let mlexpr_of_modid id =
+	<:expr< Names.id_of_string $str:string_of_id id$ >> in
+      let e = List.map mlexpr_of_modid (repr_dirpath l) in
+      let e = expr_list_of_var_list e in
+      <:expr< Coqast.Path loc (Libnames.encode_kn (Names.make_dirpath $e$)
+                (Names.id_of_string $str:Names.string_of_id a$)) >> 
   | Coqast.Dynamic (_, _) ->
       failwith "Q_Coqast: dynamic: not implemented"