diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-24 15:17:06 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-24 15:17:06 +0100 |
| commit | 15f22178b01113be7fcd603317ac7883afb6bee4 (patch) | |
| tree | 2d96805898aa01461059ed8b34ee9790122942ac /kernel/inductive.ml | |
| parent | a1a9f9d62dfe0e8dfb8c924a74e57c9f08b4f2d9 (diff) | |
| parent | 7e47c1fc1d26590ffcc89b2d3716bc749e3e1597 (diff) | |
Merge PR #486: Make some functions on terms more robust w.r.t new term constructs.
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 0782ea820..62aa9a2d7 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 |