diff options
| author | Pierre-Marie Pédrot | 2016-10-31 20:25:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-31 20:53:16 +0100 |
| commit | 19a2dd5cfbd72defe932656a65ab9da9f4ac9d1e (patch) | |
| tree | 83e0b7a05d02e7e0bd11ff8120eaf07cfcd5f08f /toplevel | |
| parent | c48838c05eea1793c2d0a11292f8fc4eb784cd02 (diff) | |
Moving unused code out of the kernel into Termops.
Strangely enough, the checker seems to rely on an outdated decompose_app
function which is not the same as the kernel, as the latter is sensitive
to casts. Cast-manipulating functions from the kernel are only used on
upper layers, and thus was moved there.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/obligations.ml | 2 | ||||
| -rw-r--r-- | toplevel/search.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index aa1a489c22..9ada043171 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -396,7 +396,7 @@ let subst_deps expand obls deps t = (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) let rec prod_app t n = - match kind_of_term (strip_outer_cast t) with + match kind_of_term (Termops.strip_outer_cast t) with | Prod (_,_,b) -> subst1 n b | LetIn (_, b, t, b') -> prod_app (subst1 b b') n | _ -> diff --git a/toplevel/search.ml b/toplevel/search.ml index 46daacb58e..d319b24199 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -112,7 +112,7 @@ let generic_search glnumopt fn = (** This function tries to see whether the conclusion matches a pattern. *) (** FIXME: this is quite dummy, we may find a more efficient algorithm. *) let rec pattern_filter pat ref env typ = - let typ = strip_outer_cast typ in + let typ = Termops.strip_outer_cast typ in if Constr_matching.is_matching env Evd.empty pat typ then true else match kind_of_term typ with | Prod (_, _, typ) @@ -120,7 +120,7 @@ let rec pattern_filter pat ref env typ = | _ -> false let rec head_filter pat ref env typ = - let typ = strip_outer_cast typ in + let typ = Termops.strip_outer_cast typ in if Constr_matching.is_matching_head env Evd.empty pat typ then true else match kind_of_term typ with | Prod (_, _, typ) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2c7fd46cf3..ede88399ef 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -107,7 +107,7 @@ let show_intro all = let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in if not (List.is_empty gls) then begin let gl = {Evd.it=List.hd gls ; sigma = sigma; } in - let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in + let l,_= decompose_prod_assum (Termops.strip_outer_cast (pf_concl gl)) in if all then let lid = Tactics.find_intro_names l gl in Feedback.msg_notice (hov 0 (prlist_with_sep spc pr_id lid)) |