From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 6 Nov 2017 23:27:09 +0100 Subject: [api] Move structures deprecated in the API to the core. We do up to `Term` which is the main bulk of the changes. --- dev/top_printers.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'dev') diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 0d833d33b5..2dae965753 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -8,6 +8,7 @@ (* Printers for the ocaml toplevel. *) +open Sorts open Util open Pp open Names @@ -17,7 +18,7 @@ open Nameops open Univ open Environ open Printer -open Term +open Constr open Evd open Goptions open Genarg @@ -242,7 +243,7 @@ let cast_kind_display k = | NATIVEcast -> "NATIVEcast" let constr_display csr = - let rec term_display c = match kind_of_term c with + let rec term_display c = match kind c with | Rel n -> "Rel("^(string_of_int n)^")" | Meta n -> "Meta("^(string_of_int n)^")" | Var id -> "Var("^(Id.to_string id)^")" @@ -314,7 +315,7 @@ let constr_display csr = open Format;; let print_pure_constr csr = - let rec term_display c = match kind_of_term c with + let rec term_display c = match Constr.kind c with | Rel n -> print_string "#"; print_int n | Meta n -> print_string "Meta("; print_int n; print_string ")" | Var id -> print_string (Id.to_string id) -- cgit v1.2.3