diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/rawterm.ml | 17 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 1 | ||||
| -rw-r--r-- | pretyping/syntax_def.ml | 11 | ||||
| -rw-r--r-- | pretyping/syntax_def.mli | 2 |
4 files changed, 11 insertions, 20 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 250fc70dc..8e46a41b2 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -193,23 +193,6 @@ let loc_of_rawconstr = function | RCast (loc,_,_) -> loc | RDynamic (loc,_) -> loc -let set_loc_of_rawconstr loc = function - | RRef (_,a) -> RRef (loc,a) - | RVar (_,a) -> RVar (loc,a) - | REvar (_,a) -> REvar (loc,a) - | RMeta (_,a) -> RMeta (loc,a) - | RApp (_,a,b) -> RApp (loc,a,b) - | RLambda (_,a,b,c) -> RLambda (loc,a,b,c) - | RProd (_,a,b,c) -> RProd (loc,a,b,c) - | RLetIn (_,a,b,c) -> RLetIn (loc,a,b,c) - | RCases (_,a,b,c,d) -> RCases (loc,a,b,c,d) - | ROldCase (_,a,b,c,d) -> ROldCase (loc,a,b,c,d) - | RRec (_,a,b,c,d) -> RRec (loc,a,b,c,d) - | RSort (_,a) -> RSort (loc,a) - | RHole (_,a) -> RHole (loc,a) - | RCast (_,a,b) -> RCast (loc,a,b) - | RDynamic (_,d) -> RDynamic (loc,d) - let join_loc (deb1,_) (_,fin2) = (deb1,fin2) type 'a raw_red_flag = { diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 5f155aa2d..04cd4da2a 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -92,7 +92,6 @@ i*) val dummy_loc : loc val loc_of_rawconstr : rawconstr -> loc -val set_loc_of_rawconstr : loc -> rawconstr -> rawconstr val join_loc : loc -> loc -> loc val subst_raw : Names.substitution -> rawconstr -> rawconstr diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml index dc5824dc7..0bb144867 100644 --- a/pretyping/syntax_def.ml +++ b/pretyping/syntax_def.ml @@ -65,4 +65,13 @@ let (in_syntax_constant, out_syntax_constant) = let declare_syntactic_definition id c = let _ = add_leaf id (in_syntax_constant c) in () -let search_syntactic_definition kn = KNmap.find kn !syntax_table +let rec set_loc loc = function + | RRef (_,a) -> RRef (loc,a) + | RVar (_,a) -> RVar (loc,a) + | RApp (_,a,b) -> RApp (loc,set_loc loc a,List.map (set_loc loc) b) + | RSort (_,a) -> RSort (loc,a) + | RHole (_,a) -> RHole (loc,a) + | a -> warning "Unrelocatated syntactic definition"; a + +let search_syntactic_definition loc kn = + set_loc loc (KNmap.find kn !syntax_table) diff --git a/pretyping/syntax_def.mli b/pretyping/syntax_def.mli index a3e1cad25..d9537cd20 100644 --- a/pretyping/syntax_def.mli +++ b/pretyping/syntax_def.mli @@ -18,6 +18,6 @@ open Rawterm val declare_syntactic_definition : identifier -> rawconstr -> unit -val search_syntactic_definition : kernel_name -> rawconstr +val search_syntactic_definition : loc -> kernel_name -> rawconstr |