diff options
Diffstat (limited to 'plugins/cc/cctac.ml')
| -rw-r--r-- | plugins/cc/cctac.ml | 39 |
1 files changed, 20 insertions, 19 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 556e6b48e6..9ea2224272 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -90,14 +90,13 @@ let rec decompose_term env sigma t= if closed0 sigma t then Symb (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) else raise Not_found (* decompose equality in members and type *) -open Termops let atom_of_constr env sigma term = let wh = whd_delta env sigma term in let kot = EConstr.kind sigma wh in match kot with App (f,args)-> - if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3 + if isRefX sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3 then `Eq (args.(0), decompose_term env sigma args.(1), decompose_term env sigma args.(2)) @@ -132,7 +131,7 @@ let non_trivial = function let patterns_of_constr env sigma nrels term= let f,args= try destApp sigma (whd_delta env sigma term) with DestKO -> raise Not_found in - if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3 + if isRefX sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3 then let patt1,rels1 = pattern_of_constr env sigma args.(1) and patt2,rels2 = pattern_of_constr env sigma args.(2) in @@ -153,7 +152,7 @@ let patterns_of_constr env sigma nrels term= let rec quantified_atom_of_constr env sigma nrels term = match EConstr.kind sigma (whd_delta env sigma term) with Prod (id,atom,ff) -> - if is_global sigma (Lazy.force _False) ff then + if isRefX sigma (Lazy.force _False) ff then let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else @@ -165,7 +164,7 @@ let rec quantified_atom_of_constr env sigma nrels term = let litteral_of_constr env sigma term= match EConstr.kind sigma (whd_delta env sigma term) with | Prod (id,atom,ff) -> - if is_global sigma (Lazy.force _False) ff then + if isRefX sigma (Lazy.force _False) ff then match (atom_of_constr env sigma atom) with `Eq(t,a,b) -> `Neq(t,a,b) | `Other(p) -> `Nother(p) @@ -277,10 +276,12 @@ let refresh_type env evm ty = Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true (Some false) env evm ty -let refresh_universes ty k = +let type_and_refresh c k = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let evm = Tacmach.New.project gl in + (* XXX is get_type_of enough? *) + let evm, ty = Typing.type_of env evm c in let evm, ty = refresh_type env evm ty in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k ty) end @@ -289,7 +290,6 @@ let constr_of_term c = EConstr.of_constr (constr_of_term c) let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> - let type_of t = Tacmach.New.pf_unsafe_type_of gl t in try (* type_of can raise exceptions *) match p.p_rule with Ax c -> exact_check (EConstr.of_constr c) @@ -297,17 +297,17 @@ let rec proof_tac p : unit Proofview.tactic = let c = EConstr.of_constr c in let l=constr_of_term p.p_lhs and r=constr_of_term p.p_rhs in - refresh_universes (type_of l) (fun typ -> + type_and_refresh l (fun typ -> app_global _sym_eq [|typ;r;l;c|] exact_check) | Refl t -> let lr = constr_of_term t in - refresh_universes (type_of lr) (fun typ -> + type_and_refresh lr (fun typ -> app_global _refl_equal [|typ;constr_of_term t|] exact_check) | Trans (p1,p2)-> let t1 = constr_of_term p1.p_lhs and t2 = constr_of_term p1.p_rhs and t3 = constr_of_term p2.p_rhs in - refresh_universes (type_of t2) (fun typ -> + type_and_refresh t2 (fun typ -> let prf = app_global_with_holes _trans_eq [|typ;t1;t2;t3;|] 2 in Tacticals.New.tclTHENS prf [(proof_tac p1);(proof_tac p2)]) | Congr (p1,p2)-> @@ -315,9 +315,9 @@ let rec proof_tac p : unit Proofview.tactic = and tx1=constr_of_term p2.p_lhs and tf2=constr_of_term p1.p_rhs and tx2=constr_of_term p2.p_rhs in - refresh_universes (type_of tf1) (fun typf -> - refresh_universes (type_of tx1) (fun typx -> - refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx -> + type_and_refresh tf1 (fun typf -> + type_and_refresh tx1 (fun typx -> + type_and_refresh (mkApp (tf1,[|tx1|])) (fun typfx -> let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in let appx1 = mkLambda(make_annot (Name id) Sorts.Relevant,typf,mkApp(mkRel 1,[|tx1|])) in let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in @@ -341,8 +341,8 @@ let rec proof_tac p : unit Proofview.tactic = let tj=constr_of_term prf.p_rhs in let default=constr_of_term p.p_lhs in let special=mkRel (1+nargs-argind) in - refresh_universes (type_of ti) (fun intype -> - refresh_universes (type_of default) (fun outtype -> + type_and_refresh ti (fun intype -> + type_and_refresh default (fun outtype -> let sigma, proj = build_projection intype cstr special default gl in @@ -362,7 +362,7 @@ let refute_tac c t1 t2 p = let neweq= app_global _eq [|intype;tt1;tt2|] in Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; simplest_elim false_t] - in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k + in type_and_refresh tt1 k end let refine_exact_check c = @@ -382,7 +382,7 @@ let convert_to_goal_tac c t1 t2 p = let endt = app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in Tacticals.New.tclTHENS (neweq (assert_before (Name e))) [proof_tac p; endt refine_exact_check] - in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k + in type_and_refresh tt2 k end let convert_to_hyp_tac c1 t1 c2 t2 p = @@ -401,7 +401,8 @@ let discriminate_tac cstru p = 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 evm = Tacmach.New.project gl in - let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl lhs) in + let evm, intype = Typing.type_of env evm lhs in + let evm, intype = refresh_type env evm intype in let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in let neweq=app_global _eq [|intype;lhs;rhs|] in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) @@ -515,7 +516,7 @@ let f_equal = in Proofview.tclORELSE begin match EConstr.kind sigma concl with - | App (r,[|_;t;t'|]) when is_global sigma (Lazy.force _eq) r -> + | App (r,[|_;t;t'|]) when isRefX sigma (Lazy.force _eq) r -> begin match EConstr.kind sigma t, EConstr.kind sigma t' with | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') -> let rec cuts i = |