diff options
| author | Xavier Leroy | 2019-07-11 09:26:10 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-01-08 15:07:15 +0100 |
| commit | ef7a95e2ca705f0fd72f15e7352eb77bf9c6eaed (patch) | |
| tree | 9fec68c2356412b4132ce1157e95986125710697 /plugins/extraction/common.ml | |
| parent | bfb28c7720d9101e2caedff0c1f1f2cdbf0bad65 (diff) | |
Support extraction of Coq's string type to OCaml's string type, continued
Address issues found in CI testing and in code review.
Diffstat (limited to 'plugins/extraction/common.ml')
| -rw-r--r-- | plugins/extraction/common.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 099a22408a..4ab1ac2fba 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -692,7 +692,7 @@ let is_native_string c = (* Extract the underlying string. *) -let rec get_native_string c = +let get_native_string c = let buf = Buffer.create 64 in let rec get = function (* "EmptyString" constructor *) |