aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--contrib/extraction/extraction.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index a6565aa87..dae19f796 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -809,6 +809,7 @@ let extract_fixpoint env vkn (fi,ti,ci) =
types.(i) <- t;
end
done;
+ current_fixpoints := [];
Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types)
let extract_constant env kn cb =