diff options
| -rw-r--r-- | contrib/extraction/mlutil.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 0c51da1ede..460e661e0f 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -993,10 +993,10 @@ let is_ind = function | IndRef _ -> true | _ -> false -let is_rec_principle = function - | ConstRef c -> - let m,d,l = repr_kn c in - let s = string_of_label l in +let is_rec_principle r = match r with + | ConstRef _ -> + let d,i = repr_qualid (shortest_qualid_of_global None r) in + let s = string_of_id i in if Filename.check_suffix s "_rec" then let i' = id_of_string (Filename.chop_suffix s "_rec") in (try is_ind (locate (make_qualid d i')) |