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. --- engine/termops.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'engine/termops.ml') diff --git a/engine/termops.ml b/engine/termops.ml index 67533cce4..78dbdb11a 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -12,6 +12,7 @@ open Util open Names open Nameops open Term +open Constr open Vars open Environ @@ -46,7 +47,7 @@ let pr_puniverses p u = if Univ.Instance.is_empty u then p else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" -let rec pr_constr c = match kind_of_term c with +let rec pr_constr c = match kind c with | Rel n -> str "#"++int n | Meta n -> str "Meta(" ++ int n ++ str ")" | Var id -> pr_id id @@ -798,7 +799,7 @@ let fold_constr_with_binders sigma g f n acc c = let iter_constr_with_full_binders g f l c = let open RelDecl in - match kind_of_term c with + match kind c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> () | Cast (c,_, t) -> f l c; f l t @@ -983,9 +984,9 @@ let isMetaOf sigma mv c = match EConstr.kind sigma c with Meta mv' -> Int.equal mv mv' | _ -> false let rec subst_meta bl c = - match kind_of_term c with + match kind c with | Meta i -> (try Int.List.assoc i bl with Not_found -> c) - | _ -> map_constr (subst_meta bl) c + | _ -> Constr.map (subst_meta bl) c let rec strip_outer_cast sigma c = match EConstr.kind sigma c with | Cast (c,_,_) -> strip_outer_cast sigma c -- cgit v1.2.3