let module T = CicTypeChecker in
let _,metasenv,_,_ = proof in
let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
- let use_auto, auto =
+ let auto =
match auto with
- | None -> false, default_auto
- | Some auto -> true, auto in
+ | None -> default_auto
+ | Some auto -> auto in
(* if use_auto is true, we try to close the hypothesis of equational
statements using auto; a naif, and probably wrong approach *)
let rec aux cache index newmeta = function
(Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
let do_find context term =
match term with
- | C.Prod (name, s, t) when (is_an_equality t && use_auto) ->
+ | C.Prod (name, s, t) when is_an_equality t ->
(try
let term = S.lift index term in
let saturated,cache,newmeta =
let candidates = List.map utty_of_u eqs in
let candidates = List.filter is_monomorphic_eq candidates in
let candidates = List.filter is_var_free candidates in
- let use_auto, auto =
+ let auto =
match auto with
- | None -> false, default_auto
- | Some auto -> true, auto in
+ | None -> default_auto
+ | Some auto -> auto in
(* if use_auto is true, we try to close the hypothesis of equational
statements using auto; a naif, and probably wrong approach *)
let rec aux cache newmeta = function
(CicPp.ppterm term) (CicPp.ppterm termty)));
let res, newmeta, cache =
match termty with
- | C.Prod (name, s, t) when use_auto ->
+ | C.Prod (name, s, t) ->
(try
let saturated,cache,newmeta =
close_hypothesis_of_term context metasenv newmeta termty
eqs, newmeta , cache
with AutoFailure (cache,newmeta) ->
[], newmeta , cache)
- | C.Prod _ -> [], newmeta, cache
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2] ->
let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in
[e], newmeta+1, cache