diff options
Diffstat (limited to 'contrib/extraction/extraction.ml')
| -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 2788fa8113..1e8b8248f2 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -595,7 +595,7 @@ and extract_constr_with_type env ctx c t = | Tarity -> Emltype (Miniml.Tarity, [], []) | Tmltype (t, sign, fl) -> Emltype (t, sign, fl)) | (Info, NotArity) -> - (match extract_term env ctx c with + (match extract_term_with_type env ctx c t with | Rmlterm a -> Emlterm a | Rprop -> Eprop) |