diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/rawterm.ml | 21 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 4 |
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 (* |