diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 08:11:07 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-22 11:33:57 +0100 |
| commit | 88afd8a9853c772b6b1681c7ae208e55e7daacbe (patch) | |
| tree | 7561c915ee289a94ea29ff5538fbafa004f4e901 /pretyping | |
| parent | 23f0f5fe6b510d2ab91a2917eb895faa479d9fcf (diff) | |
[api] Deprecate Term destructors, move to Constr
We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.
This is a step towards having a single module for `Constr`.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 3 | ||||
| -rw-r--r-- | pretyping/evardefine.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 2 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 2 |
4 files changed, 4 insertions, 5 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 681eb17d3..18e0c31dd 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -9,7 +9,6 @@ open CErrors open Util open Names -open Term open Constr open Termops open Environ @@ -49,7 +48,7 @@ let _ = Goptions.declare_bool_option { "data.id.type" etc... *) let impossible_default_case () = let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in - let (_, u) = Term.destConst c in + let (_, u) = Constr.destConst c in Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx) let coq_unit_judge = diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 18dbbea1b..b646a37f8 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Sorts open Util open Pp open Names -open Term open Constr open Termops open EConstr diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index fba154291..e6d1e59b3 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Sorts open Util open CErrors open Names -open Term open Constr open Environ open Termops diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index e6d8a0af2..9ff9a75b3 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -213,7 +213,7 @@ let compute_canonical_projections warn (con,ind) = let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let t = EConstr.Unsafe.to_constr t in let lt = List.rev_map snd sign in - let args = snd (Term.decompose_app t) in + let args = snd (decompose_app t) in let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in let params, projs = List.chop p args in |