Commit 16baee25 authored by Simon Cruanes's avatar Simon Cruanes
Browse files

bugfix du à un changement de l'api de Term

parent dfa35b47
......@@ -220,7 +220,7 @@ module Translate = struct
| FQuant (quant, vars, f) -> begin
(* Format.printf "@[<hov 2>quantifier %s %s (depth %d)@]\n" (if quant=Forall then "forall" else "exists") (String.concat ", " vars) (EnvVar.depth ()); *)
EnvVar.push_scope vars; (* new scope *)
let answer = Term.f_quant
let answer = Term.f_quant_close
(translate_quant quant)
(List.map EnvVar.find vars)
[] (* no triggers *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment