*** empty log message ***

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

2 files changed, 25 insertions, 0 deletions

diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 8ea4a25c3d..77afa80410 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -27,6 +27,10 @@ type cases_pattern =
   | PatVar of loc * name
   | PatCstr of loc * constructor * cases_pattern list * name
 
+let pattern_loc = function
+    PatVar(loc,_) -> loc
+  | PatCstr(loc,_,_,_) -> loc
+
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
 type fix_kind = RFix of (int array * int) | RCoFix of int
@@ -83,6 +87,23 @@ type rawconstr =
    - boolean in POldCase means it is recursive
 i*)
 
+let loc = function
+  | RVar (loc,_) -> loc
+  | RApp (loc,_,_) -> loc
+  | RLambda (loc,_,_,_) -> loc
+  | RProd (loc,_,_,_) -> loc
+  | RLetIn (loc,_,_,_) -> loc
+  | RCases (loc,_,_,_) -> loc
+  | ROrderedCase (loc,_,_,_,_) -> loc
+  | RRec (loc,_,_,_,_) -> loc
+  | RCast (loc,_,_) -> loc
+  | RSort (loc,_) -> loc
+  | RHole (loc,_) -> loc
+  | RRef (loc,_) -> loc
+  | REvar (loc,_) -> loc
+  | RMeta (loc,_) -> loc
+  | RDynamic (loc,_) -> loc
+
 let map_rawconstr f = function
   | RVar (loc,id) -> RVar (loc,id)
   | RApp (loc,g,args) -> RApp (loc,f g, List.map f args)
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 981cb23314..b5e408bb54 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -27,6 +27,8 @@ type cases_pattern =
   | PatVar of loc * name
   | PatCstr of loc * constructor * cases_pattern list * name
 
+val pattern_loc : cases_pattern -> loc
+
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
 type fix_kind = RFix of (int array * int) | RCoFix of int
@@ -84,6 +86,8 @@ type rawconstr =
    - option in PHole tell if the "?" was apparent or has been implicitely added
 i*)
 
+val loc : rawconstr -> loc
+
 val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr
 
 (*