diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 19:22:24 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 20:41:05 +0200 |
| commit | b6e39ade125862ba41ca17b06b8e35726b9b0d7d (patch) | |
| tree | 4faa9cbbc56f3b63f5ef89f98452ab69b31af887 /pretyping/tacred.ml | |
| parent | 02b66da78e766a0eb8a1ec82a03ec9ce5418a0f0 (diff) | |
Fix semantics of matching with folded/unfolded projections to definitely
avoid looping and be compatible with unfold.
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index ab04a9045..bddd274ef 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -799,9 +799,6 @@ and whd_construct_stack env sigma s = sequence of products; fails if no delta redex is around *) -let match_eval_proj env proj = - ((lookup_constant proj env).Declarations.const_proj) - let try_red_product env sigma c = let simpfun = clos_norm_flags betaiotazeta env sigma in let rec redrec env x = |