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 /tactics/hints.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 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index ace51c40d4..0cc8becd8f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -46,7 +46,7 @@ let rec head_bound sigma t = match EConstr.kind sigma t with | Prod (_, _, b) -> head_bound sigma b | LetIn (_, _, _, b) -> head_bound sigma b | App (c, _) -> head_bound sigma c -| Case (_, _, _, c, _) -> head_bound sigma c +| Case (_, _, _, _, _, c, _) -> head_bound sigma c | Ind (ind, _) -> GlobRef.IndRef ind | Const (c, _) -> GlobRef.ConstRef c | Construct (c, _) -> GlobRef.ConstructRef c @@ -591,7 +591,7 @@ struct let head_evar sigma c = let rec hrec c = match EConstr.kind sigma 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 |