Commit a3ba5e5f authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

update coq-plugin

parent 134580a4
......@@ -689,11 +689,11 @@ and tr_term dep tvm bv env t =
let ls = tr_global_ls dep env (ConstructRef cj) in
if List.length vars <> List.length ls.ls_args then raise NotFO;
let pat = pat_app ls (List.map pat_var vars) ty in
pat, tr_term dep tvm bv env bj
t_close_branch pat (tr_term dep tvm bv env bj)
in
let ty = type_of env Evd.empty t in
let ty = tr_type dep tvm env ty in
t_case e (Array.to_list (Array.mapi branch br)) ty
t_case e (Array.to_list (Array.mapi branch br))
| _ ->
let f, cl = decompose_app t in
let r = global_of_constr f in
......@@ -795,12 +795,12 @@ and tr_formula dep tvm bv env f =
(tr_formula dep tvm bv env a) (tr_formula dep tvm bv env b)
else
let vs, _t, bv, env, b = quantifiers n a b dep tvm bv env in
Term.f_forall [vs] [] (tr_formula dep tvm bv env b)
Term.f_forall_close [vs] [] (tr_formula dep tvm bv env b)
| _, [_; a] when c = build_coq_ex () ->
begin match kind_of_term a with
| Lambda(n, a, b) ->
let vs, _t, bv, env, b = quantifiers n a b dep tvm bv env in
Term.f_exists [vs] [] (tr_formula dep tvm bv env b)
Term.f_exists_close [vs] [] (tr_formula dep tvm bv env b)
| _ ->
(* unusual case of the shape (ex p) *)
(* TODO: we could eta-expanse *)
......@@ -821,7 +821,7 @@ and tr_formula dep tvm bv env f =
let ls = tr_global_ls dep env (ConstructRef cj) in
if List.length vars <> List.length ls.ls_args then raise NotFO;
let pat = pat_app ls (List.map pat_var vars) ty in
pat, tr_formula dep tvm bv env bj
f_close_branch pat (tr_formula dep tvm bv env bj)
in
f_case t (Array.to_list (Array.mapi branch br))
| Case _, _ :: _ ->
......@@ -856,7 +856,7 @@ let tr_goal gl =
let ty = tr_type dep tvm env ty in (* DO NOT INLINE! *)
let vs = Term.create_vsymbol (preid_of_id id) ty in
let bv = Idmap.add id vs bv in
Term.f_forall [vs] [] (tr_ctxt tvm bv ctxt)
Term.f_forall_close [vs] [] (tr_ctxt tvm bv ctxt)
else if is_Prop t then
let h = tr_formula dep tvm bv env ty in (* DO NOT INLINE! *)
Term.f_implies h (tr_ctxt tvm bv ctxt)
......@@ -874,7 +874,7 @@ let tr_goal gl =
let ty = tr_type dep tvm env ty in
let vs = Term.create_vsymbol (preid_of_id id) ty in
let bv = Idmap.add id vs bv in
Term.f_let vs d (tr_ctxt tvm bv ctxt)
Term.f_let_close vs d (tr_ctxt tvm bv ctxt)
with NotFO ->
tr_ctxt tvm bv ctxt
end
......
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