aboutsummaryrefslogtreecommitdiff
path: root/src/tac2intern.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-08-18 17:03:37 +0200
committerPierre-Marie Pédrot2017-08-18 17:06:06 +0200
commit33f7df93bb686077b9ca164078763c2208cbe3d5 (patch)
tree01da01f1bc5bd160f4599eafd6fc97acc38ada71 /src/tac2intern.ml
parentf392ad50331d3e59d3e2f3ec66c0a42112506d7f (diff)
Removing dead code.
Diffstat (limited to 'src/tac2intern.ml')
-rw-r--r--src/tac2intern.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index bf7e93cb9e..b62a574a6c 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -24,7 +24,6 @@ let coq_type n = KerName.make2 Tac2env.coq_prefix (Label.make n)
let t_int = coq_type "int"
let t_string = coq_type "string"
let t_array = coq_type "array"
-let t_unit = coq_type "unit"
let t_list = coq_type "list"
let c_nil = GTacCst (Other t_list, 0, [])