aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/nsatz/nsatz.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/nsatz/nsatz.ml4')
-rw-r--r--plugins/nsatz/nsatz.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index 97db0f731..4cac90713 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -420,7 +420,7 @@ let pol_sparse_to_term n2 p =
aux p
-let rec remove_list_tail l i =
+let remove_list_tail l i =
let rec aux l i =
if l=[]
then []