We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 31720a0 commit 6c1473eCopy full SHA for 6c1473e
src/core/libTerm.ml
@@ -175,11 +175,12 @@ let fold (x:var) (t:term): term -> term =
175
match unfold u with
176
| Appl(a,b) -> mk_Appl(aux a, aux b)
177
| Abst(a,b) ->
178
- let x,b = Term.unbind b in mk_Abst(aux a, Term.bind_var x b)
+ let x,b = Term.unbind b in mk_Abst(aux a, Term.bind_var x (aux b))
179
| Prod(a,b) ->
180
- let x,b = Term.unbind b in mk_Prod(aux a, Term.bind_var x b)
+ let x,b = Term.unbind b in mk_Prod(aux a, Term.bind_var x (aux b))
181
| LLet(a,d,b) ->
182
- let x,b = Term.unbind b in mk_LLet(aux a, aux d, Term.bind_var x b)
+ let x,b = Term.unbind b in
183
+ mk_LLet(aux a, aux d, Term.bind_var x (aux b))
184
| Meta(m,us) -> mk_Meta(m,Array.map aux us)
185
| _ -> u
186
in
0 commit comments