diff options
| author | Pierre-Marie Pédrot | 2019-03-03 21:03:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-04 14:00:20 +0100 |
| commit | d72e5c154faeea1d55387bc8c039d97f63ebd1c4 (patch) | |
| tree | d7f3c292606e98d2c2891354398e8d406d4dc15c /vernac/comDefinition.ml | |
| parent | 6632739f853e42e5828fbf603f7a3089a00f33f7 (diff) | |
Change the representation of kernel case.
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index c54adb45f9..b3ffb864f2 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -69,9 +69,10 @@ let protect_pattern_in_binder bl c ctypopt = | LetIn (x,b,t,c) -> let evd,c = aux (push_rel (LocalDef (x,b,t)) env) evd c in evd, mkLetIn (x,t,b,c) - | Case (ci,p,iv,a,bl) -> + | Case (ci,u,pms,p,iv,a,bl) -> + let (ci, p, iv, a, bl) = EConstr.expand_case env evd (ci, u, pms, p, iv, a, bl) in let evd,bl = Array.fold_left_map (aux env) evd bl in - evd, mkCase (ci,p,iv,a,bl) + evd, mkCase (EConstr.contract_case env evd (ci, p, iv, a, bl)) | Cast (c,_,_) -> f env evd c (* we remove the cast we had set *) (* This last case may happen when reaching the proof of an impossible case, as when pattern-matching on a vector of length 1 *) |