Commit 1ec65bb9 authored by Sylvain Dailler's avatar Sylvain Dailler

Remove invalid usage of Opt.map

parent 10306ad1
...@@ -76,13 +76,15 @@ let revert ?tr g d : Term.term = ...@@ -76,13 +76,15 @@ let revert ?tr g d : Term.term =
| Ddata _ -> raise (Arg_trans "revert: cannot revert type") | Ddata _ -> raise (Arg_trans "revert: cannot revert type")
| Dparam ls -> | Dparam ls ->
(try (try
let attrs = Opt.map2 (fun tr ls -> tr ls) tr (Some ls) in let attrs = match tr with
let new_ident = Ident.id_fresh ?attrs ls.ls_name.Ident.id_string in | None -> None
let new_var = Term.create_vsymbol new_ident (Opt.get ls.Term.ls_value) in | Some tr -> Some (tr ls) in
let g = t_replace (t_app_infer ls []) (t_var new_var) g in let new_ident = Ident.id_fresh ?attrs ls.ls_name.Ident.id_string in
t_forall_close [new_var] [] g let new_var = Term.create_vsymbol new_ident (Opt.get ls.Term.ls_value) in
with let g = t_replace (t_app_infer ls []) (t_var new_var) g in
| _ -> raise (Arg_trans ("revert: cannot revert:" ^ ls.ls_name.Ident.id_string))) t_forall_close [new_var] [] g
with
| e -> raise (Arg_trans ("revert: cannot revert:" ^ ls.ls_name.Ident.id_string)))
(* TODO extend this *) (* TODO extend this *)
| Dlogic _ -> | Dlogic _ ->
raise (Arg_trans "revert: cannot revert logic decls") raise (Arg_trans "revert: cannot revert logic decls")
......
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