6 files changed, 56 insertions, 54 deletions
diff --git a/parsing/ast.ml b/parsing/ast.ml
index e366600c83..eef1ca4b74 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -588,22 +588,3 @@ let rec occur_var_ast s = function
   | Slam(_,sopt,body) -> (Some s <> sopt) & occur_var_ast s body
   | Id _ | Str _ | Num _ | Path _ | ConPath _ -> false
   | Dynamic _ -> (* Hum... what to do here *) false
-
-
-(**********************************************************************)
-(* Object substitution in modules *)
-
-let rec subst_astpat subst = function
-  | Pquote a -> Pquote (subst_ast subst a)
-  | Pmeta _ as p -> p
-  | Pnode (s,pl) -> Pnode (s,subst_astpatlist subst pl)
-  | Pslam (ido,p) -> Pslam (ido,subst_astpat subst p)
-  | Pmeta_slam (s,p) -> Pmeta_slam (s,subst_astpat subst p)
-
-and subst_astpatlist subst = function
-  | Pcons (p,pl) -> Pcons (subst_astpat subst p, subst_astpatlist subst pl)
-  | (Plmeta _ | Pnil) as pl -> pl
-
-let subst_pat subst = function
-  | AstListPat pl -> AstListPat (subst_astpatlist subst pl)
-  | PureAstPat p -> PureAstPat (subst_astpat subst p)
diff --git a/parsing/ast.mli b/parsing/ast.mli
index b915c65523..9c7eec43ca 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -46,7 +46,7 @@ val meta_of_ast : Coqast.t -> string
 
 (* patterns of ast *)
 type astpat =
-  | Pquote of t
+  | Pquote of Coqast.t
   | Pmeta of string * tok_kind
   | Pnode of string * patlist
   | Pslam of identifier option * astpat
@@ -119,6 +119,3 @@ val find_all_matches : ('a -> astpat) -> env -> t -> 'a list -> ('a * env) list
 val first_matchl : ('a -> patlist) -> env -> Coqast.t list -> 'a list ->
   ('a * env) option
 val to_pat : entry_env -> Coqast.t -> (astpat * entry_env)
-
-(* Object substitution in modules *)
-val subst_astpat : substitution -> astpat -> astpat
diff --git a/parsing/coqast.ml b/parsing/coqast.ml
index a80982f8ac..3811dd322a 100644
--- a/parsing/coqast.ml
+++ b/parsing/coqast.ml
@@ -102,31 +102,3 @@ 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,hconpath) in
   (hast,hloc)
-
-let rec subst_ast subst ast = match ast with
-  | Node (l,s,astl) ->
-      let astl' = Util.list_smartmap (subst_ast subst) astl in
-	if astl' == astl then ast else
-	  Node (l,s,astl')
-  | Slam (l,ido,ast1) ->
-      let ast1' = subst_ast subst ast1 in
-	if ast1' == ast1 then ast else
-	  Slam (l,ido,ast1')
-  | Smetalam (l,s,ast1) ->
-      let ast1' = subst_ast subst ast1 in
-	if ast1' == ast1 then ast else
-	  Smetalam (l,s,ast1')
-  | Path (loc,kn) -> 
-      let kn' = subst_kn subst kn in
-	if kn' == kn then ast else
-	  Path(loc,kn')
-  | ConPath (loc,kn) -> 
-      let kn' = subst_con subst kn in
-	if kn' == kn then ast else
-	  ConPath(loc,kn')
-  | Nmeta _
-  | Nvar _ -> ast
-  | Num _
-  | Str _
-  | Id _
-  | Dynamic _ -> ast
diff --git a/parsing/coqast.mli b/parsing/coqast.mli
index a769c66f96..b588d9cea0 100644
--- a/parsing/coqast.mli
+++ b/parsing/coqast.mli
@@ -12,7 +12,6 @@
 open Util
 open Names
 open Libnames
-open Mod_subst
 (*i*)
 
 (* Abstract syntax trees. *)
@@ -43,8 +42,6 @@ val hcons_ast:
   * (kernel_name -> kernel_name) * (constant -> constant)
   -> (t -> t) * (loc -> loc)
 
-val subst_ast: substitution -> t -> t
-
 (*
 val map_tactic_expr : (t -> t) -> (tactic_expr -> tactic_expr) -> tactic_expr -> tactic_expr
 val fold_tactic_expr :
diff --git a/parsing/termast.ml b/parsing/termast.ml
index efa6c92068..ace1b47d20 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -26,6 +26,7 @@ open Ast
 open Rawterm
 open Pattern
 open Nametab
+open Mod_subst
 
 (* In this file, we translate rawconstr to ast, in order to print constr *)
 
@@ -390,6 +391,55 @@ let ast_of_constr at_top env t =
   ast_of_raw 
     (Detyping.detype (at_top,env) avoid (names_of_rel_context env) t')
 
+(**********************************************************************)
+(* Object substitution in modules *)
+
+let rec subst_ast subst ast = match ast with
+  | Node (l,s,astl) ->
+      let astl' = Util.list_smartmap (subst_ast subst) astl in
+	if astl' == astl then ast else
+	  Node (l,s,astl')
+  | Slam (l,ido,ast1) ->
+      let ast1' = subst_ast subst ast1 in
+	if ast1' == ast1 then ast else
+	  Slam (l,ido,ast1')
+  | Smetalam (l,s,ast1) ->
+      let ast1' = subst_ast subst ast1 in
+	if ast1' == ast1 then ast else
+	  Smetalam (l,s,ast1')
+  | Path (loc,kn) -> 
+      let kn' = subst_kn subst kn in
+	if kn' == kn then ast else
+	  Path(loc,kn')
+  | ConPath (loc,kn) -> 
+      let kn',t = subst_con subst kn in
+	if kn' == kn then ast else
+	  ast_of_constr false (Global.env ()) t
+  | Nmeta _
+  | Nvar _ -> ast
+  | Num _
+  | Str _
+  | Id _
+  | Dynamic _ -> ast
+
+let rec subst_astpat subst = function
+(*CSC: this is wrong since I am not recompiling the whole pattern.
+  However, this is V7-syntax code that is doomed to disappear. Hence I
+  prefer to be lazy and to not fix the bug. *)
+  | Pquote a -> Pquote (subst_ast subst a)
+  | Pmeta _ as p -> p
+  | Pnode (s,pl) -> Pnode (s,subst_astpatlist subst pl)
+  | Pslam (ido,p) -> Pslam (ido,subst_astpat subst p)
+  | Pmeta_slam (s,p) -> Pmeta_slam (s,subst_astpat subst p)
+
+and subst_astpatlist subst = function
+  | Pcons (p,pl) -> Pcons (subst_astpat subst p, subst_astpatlist subst pl)
+  | (Plmeta _ | Pnil) as pl -> pl
+
+let subst_pat subst = function
+  | AstListPat pl -> AstListPat (subst_astpatlist subst pl)
+  | PureAstPat p -> PureAstPat (subst_astpat subst p)
+
 let ast_of_constant env sp =
   let a = ast_of_constant_ref sp in
   a
diff --git a/parsing/termast.mli b/parsing/termast.mli
index f4c9466d35..da7e476bed 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -18,6 +18,7 @@ open Libnames
 open Nametab
 open Rawterm
 open Pattern
+open Mod_subst
 (*i*)
 
 (* Translation of pattern, cases pattern, rawterm and term into syntax
@@ -32,6 +33,10 @@ val ast_of_pattern : env -> names_context -> constr_pattern -> Coqast.t
 
 val ast_of_constr : bool -> env -> constr -> Coqast.t
 
+(* Object substitution in modules *)
+val subst_ast: substitution -> Coqast.t -> Coqast.t
+val subst_astpat : substitution -> Ast.astpat -> Ast.astpat
+
 val ast_of_constant     : env -> constant -> Coqast.t
 val ast_of_existential  : env -> existential -> Coqast.t
 val ast_of_constructor  : env -> constructor -> Coqast.t