Merge pull request #46 from AeneasVerif/son_improves

Minor improvements for the extraction

1 files changed, 5 insertions, 1 deletions

diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 41c81207..a916bffb 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -61,7 +61,10 @@ let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) :
               | TArray -> "Array"
               | TSlice -> "Slice"
             else expr_to_string c ty
-        | ERef _ | EVar _ -> raise (Failure ""))
+        | ERef _ | EVar _ ->
+            (* We simply convert the pattern to a string. This is not very
+               satisfying but we should rarely get there. *)
+            expr_to_string c ty)
   in
   let rec pattern_to_string (n : pattern) : string list =
     match n with
@@ -73,6 +76,7 @@ let pattern_to_extract_name (is_trait_impl : bool) (name : pattern) :
   in
   pattern_to_string name
 
+let pattern_to_type_extract_name = pattern_to_extract_name false
 let pattern_to_fun_extract_name = pattern_to_extract_name false
 let pattern_to_trait_impl_extract_name = pattern_to_extract_name true