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, 12 insertions, 4 deletions

diff --git a/parsing/coqast.ml b/parsing/coqast.ml
index 71dfd9547f..52681fe342 100644
--- a/parsing/coqast.ml
+++ b/parsing/coqast.ml
@@ -24,6 +24,7 @@ type t =
   | Str of loc * string
   | Id of loc * string
   | Path of loc * kernel_name
+  | ConPath of loc * constant
   | Dynamic of loc * Dyn.t
 
 type the_coq_ast = t
@@ -62,8 +63,9 @@ module Hast = Hashcons.Make(
     type u = 
 	(the_coq_ast -> the_coq_ast) *
 	((loc -> loc) * (string -> string)
-	 * (identifier -> identifier) * (kernel_name -> kernel_name))
-    let hash_sub (hast,(hloc,hstr,hid,hsp)) = function
+	 * (identifier -> identifier) * (kernel_name -> kernel_name)
+         * (constant -> constant))
+    let hash_sub (hast,(hloc,hstr,hid,hsp,hcon)) = function
       | Node(l,s,al) -> Node(hloc l, hstr s, List.map hast al)
       | Nmeta(l,s) -> Nmeta(hloc l, hstr s)
       | Nvar(l,s) -> Nvar(hloc l, hid s)
@@ -74,6 +76,7 @@ module Hast = Hashcons.Make(
       | Id(l,s) -> Id(hloc l, hstr s)
       | Str(l,s) -> Str(hloc l, hstr s)
       | Path(l,d) -> Path(hloc l, hsp d)
+      | ConPath(l,d) -> ConPath(hloc l, hcon d)
       | Dynamic(l,d) -> Dynamic(hloc l, d)
     let equal a1 a2 =
       match (a1,a2) with
@@ -89,13 +92,14 @@ module Hast = Hashcons.Make(
         | (Id(l1,s1), Id(l2,s2)) -> l1==l2 & s1==s2
         | (Str(l1,s1),Str(l2,s2)) -> l1==l2 & s1==s2
         | (Path(l1,d1), Path(l2,d2)) -> (l1==l2 & d1==d2)
+        | (ConPath(l1,d1), ConPath(l2,d2)) -> (l1==l2 & d1==d2)
         | _ -> false
     let hash = Hashtbl.hash
   end)
 
-let hcons_ast (hstr,hid,hpath) =
+let hcons_ast (hstr,hid,hpath,hconpath) =
   let hloc = Hashcons.simple_hcons Hloc.f () in
-  let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr,hid,hpath) in
+  let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr,hid,hpath,hconpath) in
   (hast,hloc)
 
 let rec subst_ast subst ast = match ast with
@@ -115,6 +119,10 @@ let rec subst_ast subst ast = match ast with
       let kn' = Names.subst_kn subst kn in
 	if kn' == kn then ast else
 	  Path(loc,kn')
+  | ConPath (loc,kn) -> 
+      let kn' = Names.subst_con subst kn in
+	if kn' == kn then ast else
+	  ConPath(loc,kn')
   | Nmeta _
   | Nvar _ -> ast
   | Num _