diff options
| author | Pierre-Marie Pédrot | 2014-06-17 14:26:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-06-17 15:44:38 +0200 |
| commit | 90d64647d3fd5dbf5c337944dc0038f0b19b8a51 (patch) | |
| tree | b33528c72730ec541a75e3d0baaead6789f4dcb9 /plugins/funind/recdef.ml | |
| parent | d412844753ef25f4431c209f47b97b9fa498297d (diff) | |
Removing dead code.
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index d8f006f518..961266c9c4 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -10,7 +10,6 @@ open Term open Vars open Namegen open Environ -open Declareops open Entries open Pp open Names @@ -125,7 +124,6 @@ let lt = function () -> (coq_base_constant "lt") let le = function () -> (coq_base_constant "le") let ex = function () -> (coq_base_constant "ex") let nat = function () -> (coq_base_constant "nat") -let coq_sig = function () -> (coq_base_constant "sig") let iter_ref () = try find_reference ["Recdef"] "iter" with Not_found -> error "module Recdef not loaded" |