diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/indrec.ml | 4 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 1daae0236a..a6f5a729a7 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -153,7 +153,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = | [] -> None,[] | ra::rest -> (match dest_recarg ra with - | Mrec j when is_rec -> (depPvect.(j),rest) + | Mrec (_,j) when is_rec -> (depPvect.(j),rest) | Imbr _ -> Flags.if_verbose warning "Ignoring recursive call"; (None,rest) @@ -223,7 +223,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = match dest_recarg recarg with | Norec -> None | Imbr _ -> None - | Mrec i -> fvect.(i) + | Mrec (_,i) -> fvect.(i) in (match optionpos with | None -> diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 07447c5404..1a5882f4fb 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -76,7 +76,7 @@ let mis_is_recursive_subset listind rarg = List.exists (fun ra -> match dest_recarg ra with - | Mrec i -> List.mem i listind + | Mrec (_,i) -> List.mem i listind | _ -> false) rvec in array_exists one_is_rec (dest_subterms rarg) |