From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:04:58 +0200 Subject: Remove some unused values and types --- engine/termops.ml | 24 ------------------------ 1 file changed, 24 deletions(-) (limited to 'engine') diff --git a/engine/termops.ml b/engine/termops.ml index 64f4c6dc5e..29dcddbb02 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -612,30 +612,6 @@ let adjust_app_array_size f1 l1 f2 l2 = let extras,restl1 = Array.chop (len1-len2) l1 in (mkApp (f1,extras), restl1, f2, l2) -(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate - subterms of [c]; it carries an extra data [l] (typically a name - list) which is processed by [g na] (which typically cons [na] to - [l]) at each binder traversal (with name [na]); it is not recursive - and the order with which subterms are processed is not specified *) - -let map_constr_with_named_binders g f l c = match kind_of_term c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> c - | Cast (c,k,t) -> mkCast (f l c, k, f l t) - | Prod (na,t,c) -> mkProd (na, f l t, f (g na l) c) - | Lambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c) - | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c) - | App (c,al) -> mkApp (f l c, Array.map (f l) al) - | Proj (p,c) -> mkProj (p, f l c) - | Evar (e,al) -> mkEvar (e, Array.map (f l) al) - | Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl) - | Fix (ln,(lna,tl,bl)) -> - let l' = Array.fold_left (fun l na -> g na l) l lna in - mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) - | CoFix(ln,(lna,tl,bl)) -> - let l' = Array.fold_left (fun l na -> g na l) l lna in - mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) - (* [map_constr_with_binders_left_to_right g f n c] maps [f n] on the immediate subterms of [c]; it carries an extra data [n] (typically a lift index) which is processed by [g] (which typically add 1 to -- cgit v1.2.3 From 528c237b658dbba896a1fe0041990cc7fec9c4c8 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:07:32 +0200 Subject: Add [_] prefix to unused values which maybe should be kept --- engine/universes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine') diff --git a/engine/universes.ml b/engine/universes.ml index ad5ff827bd..ab561784c3 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -732,7 +732,7 @@ let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cs type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t -let pr_constraints_map cmap = +let _pr_constraints_map (cmap:constraints_map) = LMap.fold (fun l cstrs acc -> Level.pr l ++ str " => " ++ prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ -- cgit v1.2.3 From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 20:11:47 +0200 Subject: Remove unused [open] statements --- engine/eConstr.ml | 1 - engine/eConstr.mli | 1 - engine/evarutil.ml | 1 - engine/evd.ml | 4 ---- engine/proofview.mli | 1 - engine/termops.ml | 1 - engine/universes.ml | 1 - 7 files changed, 10 deletions(-) (limited to 'engine') diff --git a/engine/eConstr.ml b/engine/eConstr.ml index bb9075e74a..54d3ce6cf7 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open CSig open CErrors open Util open Names diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 3a9469e55a..693b592fd4 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -9,7 +9,6 @@ open CSig open Names open Constr -open Context open Environ type t diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 1624dc93e4..fba4661074 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -10,7 +10,6 @@ open CErrors open Util open Names open Term -open Vars open Termops open Namegen open Pre_env diff --git a/engine/evd.ml b/engine/evd.ml index 5419a10a8e..6b1e1a855f 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -14,8 +14,6 @@ open Nameops open Term open Vars open Environ -open Globnames -open Context.Named.Declaration module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -360,8 +358,6 @@ module EvMap = Evar.Map module EvNames : sig -open Misctypes - type t val empty : t diff --git a/engine/proofview.mli b/engine/proofview.mli index a3b0304b17..da8a8fecdd 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -13,7 +13,6 @@ state and returning a value of type ['a]. *) open Util -open Term open EConstr (** Main state of tactics *) diff --git a/engine/termops.ml b/engine/termops.ml index 29dcddbb02..19e62f8e62 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1427,7 +1427,6 @@ let dependency_closure env sigma sign hyps = List.rev lh let global_app_of_constr sigma c = - let open Univ in let open Globnames in match EConstr.kind sigma c with | Const (c, u) -> (ConstRef c, u), None diff --git a/engine/universes.ml b/engine/universes.ml index ab561784c3..1900112dde 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -13,7 +13,6 @@ open Term open Environ open Univ open Globnames -open Decl_kinds let pr_with_global_universes l = try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ()))) -- cgit v1.2.3 From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Tue, 25 Apr 2017 14:31:15 +0200 Subject: Fix 4.04 warnings --- engine/evd.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index 6b1e1a855f..db048bbd6e 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -15,7 +15,7 @@ open Term open Vars open Environ -module RelDecl = Context.Rel.Declaration +(* module RelDecl = Context.Rel.Declaration *) module NamedDecl = Context.Named.Declaration (** Generic filters *) -- cgit v1.2.3