diff options
| -rw-r--r-- | contrib/extraction/extraction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 6e1cdcfccb..415921524e 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -313,7 +313,7 @@ and extract_inductive kn = try (find_structure (kn,0)).s_PROJ with Not_found -> raise (I Standard); in - let s = List.map (type_neq mlt_env Tdummy) l in + let s = List.map (type_neq mlt_env Tdummy) typ in let check (_,o) = match o with | None -> raise (I Standard) | Some kn -> ConstRef kn |