Commit d2d8a9e6 authored by Andrei Paskevich's avatar Andrei Paskevich

fix #194 in a way that really does fix it

parent 20ea9c11
Pipeline #43654 passed with stages
in 109 minutes and 37 seconds
......@@ -1602,9 +1602,9 @@ let let_defn ?(keep_loc=true) (id, ghost, kind, de) =
"Lemma-functions must have parameters"
| RKlocal, _ -> invalid_arg "Dexpr.let_defn"
let expr ?(keep_loc=true) ?(lghost=false) de =
let expr ?(keep_loc=true) ?(ughost=false) de =
let uloc = if keep_loc then None else Some None in
expr uloc {env_empty with lgh = lghost} de
expr uloc {env_empty with ugh = ughost} de
let () = Exn_printer.register (fun fmt e -> match e with
| UnboundLabel s ->
......
......@@ -191,7 +191,7 @@ val drec_defn : denv -> pre_fun_defn list -> denv * drec_defn
(** Final stage *)
val expr : ?keep_loc:bool -> ?lghost:bool -> dexpr -> expr
val expr : ?keep_loc:bool -> ?ughost:bool -> dexpr -> expr
val let_defn : ?keep_loc:bool -> dlet_defn -> let_defn
val rec_defn : ?keep_loc:bool -> drec_defn -> let_defn
......@@ -1109,7 +1109,7 @@ let add_types muc tdl =
let dity = dity_of_ity v.pv_ity in
let de = dexpr muc denv_empty e in
let de = Dexpr.dexpr ?loc:de.de_loc (DEcast (de, dity)) in
Mpv.add v (expr ~keep_loc:true ~lghost:true de) m in
Mpv.add v (expr ~keep_loc:true ~ughost:true de) m in
let wit = List.fold_left add_w Mpv.empty d.td_wit in
let wit = if d.td_wit = [] then [] else
List.map (fun (_,v) -> try Mpv.find v wit with
......
Markdown is supported
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