diff options
| author | Gaetan Gilbert | 2017-04-21 20:04:58 +0200 |
|---|---|---|
| committer | Gaetan Gilbert | 2017-04-27 21:39:25 +0200 |
| commit | 02d2f34e5c84f0169e884c07054a6fbfef9f365c (patch) | |
| tree | 5e55f22c5b20dcf694c00741a69dae6f1d993267 /plugins/funind | |
| parent | 95239fa33c5da60080833dabc3ced246680dfdf9 (diff) | |
Remove some unused values and types
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 8dae17d69e..df81bc78c4 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -19,12 +19,6 @@ open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration -let local_assum (na, t) = - RelDecl.LocalAssum (na, EConstr.Unsafe.to_constr t) - -let local_def (na, b, t) = - RelDecl.LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t) - (* let msgnl = Pp.msgnl *) (* |