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 /engine/evarutil.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 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index ba6a9ea6d9..f9f8268507 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -144,7 +144,7 @@ let head_evar sigma c = let c = EConstr.Unsafe.to_constr c in let rec hrec c = match kind c with | Evar (evk,_) -> evk - | Case (_,_,_,c,_) -> hrec c + | Case (_, _, _, _, _, c, _) -> hrec c | App (c,_) -> hrec c | Cast (c,_,_) -> hrec c | Proj (p, c) -> hrec c |