aboutsummaryrefslogtreecommitdiff
path: root/src/tac2intern.ml
diff options
context:
space:
mode:
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, [])