diff options
Diffstat (limited to 'contrib/extraction')
| -rw-r--r-- | contrib/extraction/extraction.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 6bc6673397..41619c85ff 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -354,7 +354,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let rec names_prod t = match kind_of_term t with | Prod(n,_,t) -> n::(names_prod t) | LetIn(_,_,_,t) -> names_prod t - | Cast(t,_) -> names_prod t + | Cast(t,_,_) -> names_prod t | _ -> [] in let field_names = @@ -515,7 +515,7 @@ let rec extract_term env mle mlt c args = extract_app env mle mlt (extract_fix env mle i recd) args | CoFix (i,recd) -> extract_app env mle mlt (extract_fix env mle i recd) args - | Cast (c, _) -> extract_term env mle mlt c args + | Cast (c,_,_) -> extract_term env mle mlt c args | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) |