aboutsummaryrefslogtreecommitdiff
path: root/theories/extraction/ExtrOCamlPArray.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/extraction/ExtrOCamlPArray.v')
-rw-r--r--theories/extraction/ExtrOCamlPArray.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/theories/extraction/ExtrOCamlPArray.v b/theories/extraction/ExtrOCamlPArray.v
index 67646bdb53..56d40c1d16 100644
--- a/theories/extraction/ExtrOCamlPArray.v
+++ b/theories/extraction/ExtrOCamlPArray.v
@@ -23,4 +23,3 @@ Extract Constant PArray.default => "Parray.default".
Extract Constant PArray.set => "Parray.set".
Extract Constant PArray.length => "Parray.length".
Extract Constant PArray.copy => "Parray.copy".
-Extract Constant PArray.reroot => "Parray.reroot".