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 /pretyping/reductionops.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 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 04374c88b..ba0502ca4 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1167,7 +1167,8 @@ let local_whd_state_gen flags sigma = |_ -> s else s - | x -> s + | Rel _ | Var _ | Sort _ | Prod _ | LetIn _ | Const _ | Ind _ | Proj _ -> s + in whrec @@ -1771,8 +1772,8 @@ let meta_reducible_instance evd b = let is_coerce = match s with CoerceToType -> true | _ -> false in if not is_coerce then irec g else u with Not_found -> u) - | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) -> - let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) in + | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) (* What if two nested casts? *) -> + let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) (* idem *) in (match try let g, s = Metamap.find m metas in |