diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-16 13:24:03 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-23 18:15:24 +0100 |
| commit | 39cbf75c554cd7e5228bd6cd962766e865c3f26b (patch) | |
| tree | c434651d7d17b9e268b053a40b676009189aca5b /kernel/inductive.ml | |
| parent | 22ae762fa8940028f6a3d8a5fd4147d5ca3b53b9 (diff) | |
Make some functions on terms more robust w.r.t new term constructs.
Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index cb03a4d6b..aad12207e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -809,8 +809,11 @@ let rec subterm_specif renv stack t = | Dead_code -> Dead_code | Not_subterm -> Not_subterm) + | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _ + | Construct _ | CoFix _ -> Not_subterm + + (* Other terms are not subterms *) - | _ -> Not_subterm and lazy_subterm_specif renv stack t = lazy (subterm_specif renv stack t) @@ -1193,8 +1196,8 @@ let check_one_cofix env nbfix def deftype = | Meta _ -> () | Evar _ -> List.iter (check_rec_call env alreadygrd n tree vlra) args - - | _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in + | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ + | Ind _ | Fix _ | Proj _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in let ((mind, _),_) = codomain_is_coind env deftype in let vlra = lookup_subterms env mind in |