From 4d37bb49bbeb640661748edc90904d2f9b299a74 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 9 Jan 2006 22:00:34 +0000
Subject: 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
---
 interp/constrintern.ml | 8 +-------
 interp/topconstr.ml    | 6 ++++++
 interp/topconstr.mli   | 2 ++
 3 files changed, 9 insertions(+), 7 deletions(-)

(limited to 'interp')

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 *)
-- 
cgit v1.2.3