diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-21 20:04:58 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-27 21:39:25 +0200 |
| commit | 02d2f34e5c84f0169e884c07054a6fbfef9f365c (patch) | |
| tree | 5e55f22c5b20dcf694c00741a69dae6f1d993267 /checker/declarations.ml | |
| parent | 95239fa33c5da60080833dabc3ced246680dfdf9 (diff) | |
Remove some unused values and types
Diffstat (limited to 'checker/declarations.ml')
| -rw-r--r-- | checker/declarations.ml | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index 56d437c16..ad93146d5 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -463,13 +463,6 @@ let is_opaque cb = match cb.const_body with let opaque_univ_context cb = force_lazy_constr_univs cb.const_body -let subst_rel_declaration sub (id,copt,t as x) = - let copt' = Option.smartmap (subst_mps sub) copt in - let t' = subst_mps sub t in - if copt == copt' && t == t' then x else (id,copt',t') - -let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) - let subst_recarg sub r = match r with | Norec -> r | (Mrec(kn,i)|Imbr (kn,i)) -> let kn' = subst_ind sub kn in @@ -517,10 +510,6 @@ let subst_decl_arity f g sub ar = if x' == x then ar else TemplateArity x' -let map_decl_arity f g = function - | RegularArity a -> RegularArity (f a) - | TemplateArity a -> TemplateArity (g a) - let subst_rel_declaration sub = Term.map_rel_decl (subst_mps sub) |