diff options
| -rw-r--r-- | parsing/prettyp.ml | 4 | ||||
| -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 |
5 files changed, 13 insertions, 22 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index f6b4b2c60..8a241aced 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -295,7 +295,7 @@ let print_inductive sp = (print_mutual sp) let print_syntactic_def sep kn = let l = label kn in - let c = Syntax_def.search_syntactic_definition kn in + let c = Syntax_def.search_syntactic_definition dummy_loc kn in (str" Syntactic Definition " ++ pr_lab l ++ str sep ++ pr_rawterm c ++ fnl ()) (*let print_module with_values kn = str "Module " ++ pr_id (id_of_label (label kn)) ++ fnl () ++ fnl () @@ -517,7 +517,7 @@ let fprint_var name typ = (str ("*** [" ^ name ^ " :") ++ fprtype typ ++ str "]" ++ fnl ()) let fprint_judge {uj_val=trm;uj_type=typ} = - (fprterm trm ++ str" : " ++ fprterm (body_of_type typ)) + (fprterm trm ++ str" : " ++ fprterm typ) let unfold_head_fconst = let rec unfrec k = match kind_of_term k with 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 |