diff options
| author | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 17:22:36 +0100 |
| commit | c70412ec8b0bb34b7a5607c07d34607a147d834c (patch) | |
| tree | 0cc6cd76a8f70dfd2f5b55b0db96db4de2ff07a2 /kernel/inductive.ml | |
| parent | 720ee2730684cc289cef588482323d177e0bea59 (diff) | |
| parent | 191e253d1d1ebd6c76c63b3d83f4228e46196a6e (diff) | |
Merge PR #6914: Primitive integers
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 05c5c0e821..c62d0e7ded 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -804,7 +804,7 @@ let rec subterm_specif renv stack t = | Not_subterm -> Not_subterm) | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _ - | Construct _ | CoFix _ -> Not_subterm + | Construct _ | CoFix _ | Int _ -> Not_subterm (* Other terms are not subterms *) @@ -1008,7 +1008,7 @@ let check_one_fix renv recpos trees def = check_rec_call renv stack (Term.applist(c,l)) end - | Sort _ -> + | Sort _ | Int _ -> assert (List.is_empty l) (* l is not checked because it is considered as the meta's context *) @@ -1194,7 +1194,8 @@ let check_one_cofix env nbfix def deftype = | Evar _ -> List.iter (check_rec_call env alreadygrd n tree vlra) args | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ - | Ind _ | Fix _ | Proj _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in + | Ind _ | Fix _ | Proj _ | Int _ -> + raise (CoFixGuardError (env,NotGuardedForm t)) in let ((mind, _),_) = codomain_is_coind env deftype in let vlra = lookup_subterms env mind in |