Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement dans Topconstr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7826 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 13 insertions, 19 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8dc060d794..df641ecd04 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -698,18 +698,12 @@ let extract_explicit_arg imps args =
 (**********************************************************************)
 (* Syntax extensions                                                  *)
 
-let coerce_to_id = function
-  | CRef (Ident (_,id)) -> id 
-  | c ->
-      user_err_loc (constr_loc c, "subst_rawconstr",
-        str"This expression should be a simple identifier")
-
 let traverse_binder subst id (ids,tmpsc,scopes as env) =
   try
     (* Binders bound in the notation are consider first-order object *)
     (* and binders not bound in the notation do not capture variables *)
     (* outside the notation *)
-    let id' = coerce_to_id (fst (List.assoc id subst)) in
+    let _,id' = coerce_to_id (fst (List.assoc id subst)) in
     id', (Idset.add id' ids,tmpsc,scopes)
   with Not_found ->
     id, env
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 36a5426373..771c5716b2 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -630,6 +630,12 @@ let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b)
 let mkLetInC (id,a,b)   = CLetIn (dummy_loc,id,a,b)
 let mkProdC (idl,a,b)   = CProdN (dummy_loc,[idl,a],b)
 
+let coerce_to_id = function
+  | CRef (Ident (loc,id)) -> (loc,id)
+  | a -> user_err_loc
+        (constr_loc a,"coerce_to_id",
+         str "This expression should be a simple identifier")
+
 (* Used in correctness and interface *)
 
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 84342b2209..5b9d69cd67 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -142,6 +142,8 @@ val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr
 val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
 val mkProdC : name located list * constr_expr * constr_expr -> constr_expr
 
+val coerce_to_id : constr_expr -> identifier located
+
 (* For binders parsing *)
 
 (* Includes let binders *)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 1807546688..d396854ba7 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -14,6 +14,7 @@ open Util
 open Tacexpr
 open Rawterm
 open Genarg
+open Topconstr
 
 let compute = Cbv all_flags
 
@@ -80,18 +81,18 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
           (try list_index (snd x) ids
           with Not_found -> error "no such fix variable")
       | _ -> error "cannot guess decreasing argument of fix" in
-  (id,n,Topconstr.CProdN(loc,bl,ty))
+  (id,n,CProdN(loc,bl,ty))
 
 let mk_cofix_tac (loc,id,bl,ann,ty) =
   let _ = option_app (fun (aloc,_) ->
     Util.user_err_loc
       (aloc,"Constr:mk_cofix_tac",
        Pp.str"Annotation forbidden in cofix expression")) ann in
-  (id,Topconstr.CProdN(loc,bl,ty))
+  (id,CProdN(loc,bl,ty))
 
 (* Functions overloaded by quotifier *)
 let induction_arg_of_constr c =
-  try ElimOnIdent (Topconstr.constr_loc c,snd(coerce_to_id c))
+  try ElimOnIdent (constr_loc c,snd(coerce_to_id c))
   with _ -> ElimOnConstr c
 
 (* Auxiliary grammar rules *)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 9fc833b4d6..cb45a9f453 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -620,10 +620,3 @@ let coerce_reference_to_id = function
         str "This expression should be a simple identifier")
 
 let coerce_global_to_id = coerce_reference_to_id
-
-let coerce_to_id = function
-  | CRef (Ident (loc,id)) -> (loc,id)
-  | a -> user_err_loc
-        (constr_loc a,"coerce_to_id",
-         str "This expression should be a simple identifier")
-
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 87e0c24baa..46ecd11d24 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -178,5 +178,3 @@ val find_position :
 val remove_levels : int -> unit 
 
 val coerce_global_to_id : reference -> identifier
-
-val coerce_to_id : constr_expr -> identifier located