diff options
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 3 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 31 |
2 files changed, 9 insertions, 25 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index aa71a45658..5dea4631c4 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -29,8 +29,7 @@ let debug x = let _= let gdopt= - { optsync=true; - optdepr=false; + { optdepr=false; optname="Congruence Verbose"; optkey=["Congruence";"Verbose"]; optread=(fun ()-> !cc_verbose); diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 7c5efaea3a..201726d1e6 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -397,33 +397,18 @@ let convert_to_hyp_tac c1 t1 c2 t2 p = simplest_elim false_t] end } -let discriminate_tac (cstr,u as cstru) p = +(* Essentially [assert (Heq : lhs = rhs) by proof_tac p; discriminate Heq] *) +let discriminate_tac cstru p = Proofview.Goal.enter { enter = begin fun gl -> - let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in + let lhs=constr_of_term p.p_lhs and rhs=constr_of_term p.p_rhs in let env = Proofview.Goal.env gl in - let concl = Proofview.Goal.concl gl in - let xid = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in - let identity = Universes.constr_of_global (Lazy.force _I) in - let identity = EConstr.of_constr identity in - let trivial = Universes.constr_of_global (Lazy.force _True) in - let trivial = EConstr.of_constr trivial in let evm = Tacmach.New.project gl in - let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in - let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in - let outtype = mkSort outtype in - let pred = mkLambda(Name xid,outtype,mkRel 1) in + let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl lhs) in let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in - let proj = build_projection intype cstru trivial concl gl in - let injt = app_global _f_equal - [|intype;outtype;proj;t1;t2;mkVar hid|] in - let endt k = - injt (fun injt -> - app_global _eq_rect - [|outtype;trivial;pred;identity;concl;injt|] k) in - let neweq = app_global _eq [|intype;t1;t2|] in + let neweq=app_global _eq [|intype;lhs;rhs|] in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) (Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) - [proof_tac p; endt refine_exact_check]) + [proof_tac p; Equality.discrHyp hid]) end } (* wrap everything *) @@ -457,11 +442,11 @@ let cc_tactic depth additionnal_terms = let open Glob_term in let env = Proofview.Goal.env gl in let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in - let hole = GHole (Loc.ghost, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in + let hole = CAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in let pr_missing (c, missing) = let c = Detyping.detype ~lax:true false [] env sigma c in let holes = List.init missing (fun _ -> hole) in - Printer.pr_glob_constr_env env (GApp (Loc.ghost, c, holes)) + Printer.pr_glob_constr_env env (CAst.make @@ GApp (c, holes)) in Feedback.msg_info (Pp.str "Goal is solvable by congruence but some arguments are missing."); |