diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:27:09 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:46:52 +0100 |
commit | 03e21974a3e971a294533bffb81877dc1bd270b6 (patch) | |
tree | 1b37339378f6bc93288b61f707efb6b08f992dc5 /pretyping/unification.ml | |
parent | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (diff) |
[api] Move structures deprecated in the API to the core.
We do up to `Term` which is the main bulk of the changes.
Diffstat (limited to 'pretyping/unification.ml')
-rw-r--r-- | pretyping/unification.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 01c28b5ed..be9943f33 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -12,7 +12,7 @@ open CErrors open Pp open Util open Names -open Term +open Constr open Termops open Environ open EConstr @@ -68,10 +68,10 @@ let _ = Goptions.declare_bool_option { let unsafe_occur_meta_or_existential c = let c = EConstr.Unsafe.to_constr c in - let rec occrec c = match kind_of_term c with + let rec occrec c = match Constr.kind c with | Evar _ -> raise Occur | Meta _ -> raise Occur - | _ -> iter_constr occrec c + | _ -> Constr.iter occrec c in try occrec c; false with Occur -> true @@ -79,7 +79,7 @@ let occur_meta_or_undefined_evar evd c = (** This is performance-critical. Using the evar-insensitive API changes the resulting heuristic. *) let c = EConstr.Unsafe.to_constr c in - let rec occrec c = match kind_of_term c with + let rec occrec c = match Constr.kind c with | Meta _ -> raise Occur | Evar (ev,args) -> (match evar_body (Evd.find evd ev) with @@ -609,7 +609,7 @@ let subst_defined_metas_evars sigma (bl,el) c = (** This seems to be performance-critical, and using the evar-insensitive primitives blow up the time passed in this function. *) let c = EConstr.Unsafe.to_constr c in - let rec substrec c = match kind_of_term c with + let rec substrec c = match Constr.kind c with | Meta i -> let select (j,_,_) = Int.equal i j in substrec (EConstr.Unsafe.to_constr (pi2 (List.find select bl))) |