diff options
| author | Arnaud Spiwack | 2014-10-13 12:10:29 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-16 10:23:29 +0200 |
| commit | e86f8ef50b940435da2b238792dffd0f9755a78d (patch) | |
| tree | 2a85f7139ec8c4751ae0f79ddd09e9507181940b | |
| parent | ba372c87f7a21cbc8bfcd4495bd59a04a63f7281 (diff) | |
Goal: remove dead code.
| -rw-r--r-- | proofs/goal.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index ea0d534c1a..9c79c8c812 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -151,12 +151,6 @@ let eval t env defs gl = let r = t env rdefs gl info in ( r , !rdefs ) -(* monadic bind on sensitive expressions *) -let bind e f = (); fun env rdefs goal info -> - let a = e env rdefs goal info in - let r = f a in - r env rdefs goal info - let enter f = (); fun env rdefs gl info -> let sigma = !rdefs in f env sigma (Evd.evar_concl info) gl |