diff options
Diffstat (limited to 'parsing/prettyp.ml')
| -rw-r--r-- | parsing/prettyp.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 4404c1929..648d4690d 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -411,12 +411,6 @@ let print_local_context () = in (print_var_rec env ++ print_last_const env) -let fprint_var name typ = - (str ("*** [" ^ name ^ " :") ++ fprtype typ ++ str "]" ++ fnl ()) - -let fprint_judge {uj_val=trm;uj_type=typ} = - (fprterm trm ++ str" : " ++ fprterm typ) - let unfold_head_fconst = let rec unfrec k = match kind_of_term k with | Const cst -> constant_value (Global.env ()) cst |