diff options
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 59 | ||||
| -rw-r--r-- | plugins/cc/ccalgo.mli | 2 | ||||
| -rw-r--r-- | plugins/cc/ccproof.ml | 2 | ||||
| -rw-r--r-- | plugins/cc/ccproof.mli | 2 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 204 | ||||
| -rw-r--r-- | plugins/cc/cctac.mli | 1 |
6 files changed, 155 insertions, 115 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 046ecf775b..c726fd5dea 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -123,7 +123,7 @@ module PacMap=Map.Make(PacOrd) module PafMap=Map.Make(PafOrd) type cinfo= - {ci_constr: constructor; (* inductive type *) + {ci_constr: pconstructor; (* inductive type *) ci_arity: int; (* # args *) ci_nhyps: int} (* # projectable args *) @@ -142,13 +142,13 @@ type term= let rec term_equal t1 t2 = match t1, t2 with - | Symb c1, Symb c2 -> eq_constr c1 c2 + | Symb c1, Symb c2 -> eq_constr_nounivs c1 c2 | Product (s1, t1), Product (s2, t2) -> family_eq s1 s2 && family_eq t1 t2 | Eps i1, Eps i2 -> Id.equal i1 i2 | Appli (t1, u1), Appli (t2, u2) -> term_equal t1 t2 && term_equal u1 u2 - | Constructor {ci_constr=c1; ci_arity=i1; ci_nhyps=j1}, - Constructor {ci_constr=c2; ci_arity=i2; ci_nhyps=j2} -> - Int.equal i1 i2 && Int.equal j1 j2 && eq_constructor c1 c2 + | Constructor {ci_constr=(c1,u1); ci_arity=i1; ci_nhyps=j1}, + Constructor {ci_constr=(c2,u2); ci_arity=i2; ci_nhyps=j2} -> + Int.equal i1 i2 && Int.equal j1 j2 && eq_constructor c1 c2 (* FIXME check eq? *) | _ -> false open Hashset.Combine @@ -163,7 +163,7 @@ let rec hash_term = function | Product (s1, s2) -> combine3 2 (hash_sorts_family s1) (hash_sorts_family s2) | Eps i -> combine 3 (Id.hash i) | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2) - | Constructor {ci_constr=c; ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j + | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j type ccpattern = PApp of term * ccpattern list (* arguments are reversed *) @@ -234,7 +234,7 @@ type node = module Constrhash = Hashtbl.Make (struct type t = constr - let equal = eq_constr + let equal = eq_constr_nounivs let hash = hash_constr end) module Typehash = Constrhash @@ -404,32 +404,50 @@ let _B_ = Name (Id.of_string "A") let _body_ = mkProd(Anonymous,mkRel 2,mkRel 2) let cc_product s1 s2 = - mkLambda(_A_,mkSort(Termops.new_sort_in_family s1), - mkLambda(_B_,mkSort(Termops.new_sort_in_family s2),_body_)) + mkLambda(_A_,mkSort(Universes.new_sort_in_family s1), + mkLambda(_B_,mkSort(Universes.new_sort_in_family s2),_body_)) let rec constr_of_term = function - Symb s->s + Symb s-> applist_projection s [] | Product(s1,s2) -> cc_product s1 s2 | Eps id -> mkVar id - | Constructor cinfo -> mkConstruct cinfo.ci_constr + | Constructor cinfo -> mkConstructU cinfo.ci_constr | Appli (s1,s2)-> make_app [(constr_of_term s2)] s1 and make_app l=function Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1 - | other -> applistc (constr_of_term other) l + | other -> + applist_proj other l +and applist_proj c l = + match c with + | Symb s -> applist_projection s l + | _ -> applistc (constr_of_term c) l +and applist_projection c l = + match kind_of_term c with + | Const c when Environ.is_projection (fst c) (Global.env()) -> + (match l with + | [] -> (* Expand the projection *) + let kn = fst c in + let ty,_ = Typeops.type_of_constant (Global.env ()) c in + let pb = Environ.lookup_projection kn (Global.env()) in + let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in + it_mkLambda_or_LetIn (mkProj(kn,mkRel 1)) ctx + | hd :: tl -> + applistc (mkProj (fst c, hd)) tl) + | _ -> applistc c l let rec canonize_name c = let func = canonize_name in match kind_of_term c with - | Const kn -> + | Const (kn,u) -> let canon_const = constant_of_kn (canonical_con kn) in - (mkConst canon_const) - | Ind (kn,i) -> + (mkConstU (canon_const,u)) + | Ind ((kn,i),u) -> let canon_mind = mind_of_kn (canonical_mind kn) in - (mkInd (canon_mind,i)) - | Construct ((kn,i),j) -> + (mkIndU ((canon_mind,i),u)) + | Construct (((kn,i),j),u) -> let canon_mind = mind_of_kn (canonical_mind kn) in - mkConstruct ((canon_mind,i),j) + mkConstructU (((canon_mind,i),j),u) | Prod (na,t,ct) -> mkProd (na,func t, func ct) | Lambda (na,t,ct) -> @@ -438,6 +456,9 @@ let rec canonize_name c = mkLetIn (na, func b,func t,func ct) | App (ct,l) -> mkApp (func ct,Array.smartmap func l) + | Proj(kn,c) -> + let canon_const = constant_of_kn (canonical_con kn) in + (mkProj (canon_const, func c)) | _ -> c (* rebuild a term from a pattern and a substitution *) @@ -469,7 +490,7 @@ let rec add_term state t= try Termhash.find uf.syms t with Not_found -> let b=next uf in - let trm = Termops.refresh_universes (constr_of_term t) in + let trm = constr_of_term t in let typ = pf_type_of state.gls trm in let typ = canonize_name typ in let new_node= diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 5d286c7326..0c5d6ca1fe 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -11,7 +11,7 @@ open Term open Names type cinfo = - {ci_constr: constructor; (* inductive type *) + {ci_constr: pconstructor; (* inductive type *) ci_arity: int; (* # args *) ci_nhyps: int} (* # projectable args *) diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index 5244dcf174..4e1806f5a0 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -20,7 +20,7 @@ type rule= | Refl of term | Trans of proof*proof | Congr of proof*proof - | Inject of proof*constructor*int*int + | Inject of proof*pconstructor*int*int and proof = {p_lhs:term;p_rhs:term;p_rule:rule} diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli index b8a8d229ab..50e3624d0a 100644 --- a/plugins/cc/ccproof.mli +++ b/plugins/cc/ccproof.mli @@ -16,7 +16,7 @@ type rule= | Refl of term | Trans of proof*proof | Congr of proof*proof - | Inject of proof*constructor*int*int + | Inject of proof*pconstructor*int*int and proof = private {p_lhs:term;p_rhs:term;p_rule:rule} diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index ac148fe182..783abc5d8d 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -23,21 +23,17 @@ open Pp open Errors open Util -let constant dir s = lazy (Coqlib.gen_constant "CC" dir s) - -let _f_equal = constant ["Init";"Logic"] "f_equal" - -let _eq_rect = constant ["Init";"Logic"] "eq_rect" - -let _refl_equal = constant ["Init";"Logic"] "eq_refl" - -let _sym_eq = constant ["Init";"Logic"] "eq_sym" - -let _trans_eq = constant ["Init";"Logic"] "eq_trans" - -let _eq = constant ["Init";"Logic"] "eq" - -let _False = constant ["Init";"Logic"] "False" +let reference dir s = Coqlib.gen_reference "CC" dir s + +let _f_equal = reference ["Init";"Logic"] "f_equal" +let _eq_rect = reference ["Init";"Logic"] "eq_rect" +let _refl_equal = reference ["Init";"Logic"] "eq_refl" +let _sym_eq = reference ["Init";"Logic"] "eq_sym" +let _trans_eq = reference ["Init";"Logic"] "eq_trans" +let _eq = reference ["Init";"Logic"] "eq" +let _False = reference ["Init";"Logic"] "False" +let _True = reference ["Init";"Logic"] "True" +let _I = reference ["Init";"Logic"] "I" let whd env= let infos=Closure.create_clos_infos Closure.betaiotazeta env in @@ -64,32 +60,36 @@ let rec decompose_term env sigma t= Appli(Appli(Product (sort_a,sort_b) , decompose_term env sigma a), decompose_term env sigma b) - | Construct c-> - let (mind,i_ind),i_con = c in + | Construct c -> + let (((mind,i_ind),i_con),u)= c in let canon_mind = mind_of_kn (canonical_mind mind) in let canon_ind = canon_mind,i_ind in let (oib,_)=Global.lookup_inductive (canon_ind) in let nargs=mis_constructor_nargs_env env (canon_ind,i_con) in - Constructor {ci_constr= (canon_ind,i_con); + Constructor {ci_constr= ((canon_ind,i_con),u); ci_arity=nargs; ci_nhyps=nargs-oib.mind_nparams} | Ind c -> - let mind,i_ind = c in + let (mind,i_ind),u = c in let canon_mind = mind_of_kn (canonical_mind mind) in - let canon_ind = canon_mind,i_ind in (Symb (mkInd canon_ind)) - | Const c -> + let canon_ind = canon_mind,i_ind in (Symb (mkIndU (canon_ind,u))) + | Const (c,u) -> let canon_const = constant_of_kn (canonical_con c) in - (Symb (mkConst canon_const)) + (Symb (mkConstU (canon_const,u))) + | Proj (p, c) -> + let canon_const = constant_of_kn (canonical_con p) in + (Appli (Symb (mkConst canon_const), decompose_term env sigma c)) | _ ->if closed0 t then (Symb t) else raise Not_found (* decompose equality in members and type *) +open Globnames let atom_of_constr env sigma term = let wh = (whd_delta env term) in let kot = kind_of_term wh in match kot with App (f,args)-> - if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3 + if is_global _eq f && Int.equal (Array.length args) 3 then `Eq (args.(0), decompose_term env sigma args.(1), decompose_term env sigma args.(2)) @@ -124,7 +124,7 @@ let non_trivial = function let patterns_of_constr env sigma nrels term= let f,args= try destApp (whd_delta env term) with DestKO -> raise Not_found in - if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3 + if is_global _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 @@ -145,7 +145,7 @@ let patterns_of_constr env sigma nrels term= let rec quantified_atom_of_constr env sigma nrels term = match kind_of_term (whd_delta env term) with Prod (id,atom,ff) -> - if eq_constr ff (Lazy.force _False) then + if is_global _False ff then let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else @@ -157,7 +157,7 @@ let rec quantified_atom_of_constr env sigma nrels term = let litteral_of_constr env sigma term= match kind_of_term (whd_delta env term) with | Prod (id,atom,ff) -> - if eq_constr ff (Lazy.force _False) then + if is_global _False ff then match (atom_of_constr env sigma atom) with `Eq(t,a,b) -> `Neq(t,a,b) | `Other(p) -> `Nother(p) @@ -218,13 +218,13 @@ let make_prb gls depth additionnal_terms = (* indhyps builds the array of arrays of constructor hyps for (ind largs) *) -let build_projection intype outtype (cstr:constructor) special default gls= +let build_projection intype outtype (cstr:pconstructor) special default gls= let env=pf_env gls in let (h,argv) = try destApp intype with DestKO -> (intype,[||]) in - let ind=destInd h in - let types=Inductiveops.arities_of_constructors env ind in + let ind,u=destInd h in + let types=Inductiveops.arities_of_constructors env (ind,u) in let lp=Array.length types in - let ci=pred (snd cstr) in + let ci=pred (snd(fst cstr)) in let branch i= let ti= prod_appvect types.(i) argv in let rc=fst (decompose_prod_assum ti) in @@ -243,60 +243,67 @@ let build_projection intype outtype (cstr:constructor) special default gls= let _M =mkMeta +let app_global f args k = + Tacticals.pf_constr_of_global f (fun fc -> k (mkApp (fc, args))) + +let new_app_global f args k = + Tacticals.New.pf_constr_of_global f (fun fc -> k (mkApp (fc, args))) + +let new_exact_check c = Proofview.V82.tactic (exact_check c) +let new_refine c = Proofview.V82.tactic (refine c) + let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> let type_of = Tacmach.New.pf_type_of gl in + try (* type_of can raise exceptions *) match p.p_rule with - Ax c -> Proofview.V82.tactic (exact_check c) + Ax c -> new_exact_check c | SymAx c -> Proofview.V82.tactic begin fun gls -> - let l=constr_of_term p.p_lhs and - r=constr_of_term p.p_rhs in - let typ = Termops.refresh_universes (pf_type_of gls l) in - exact_check - (mkApp(Lazy.force _sym_eq,[|typ;r;l;c|])) gls + let l=constr_of_term p.p_lhs and + r=constr_of_term p.p_rhs in + let typ = (* Termops.refresh_universes *)pf_type_of gls l in + (app_global _sym_eq [|typ;r;l;c|] exact_check) gls end | Refl t -> Proofview.V82.tactic begin fun gls -> - let lr = constr_of_term t in - let typ = Termops.refresh_universes (pf_type_of gls lr) in - exact_check - (mkApp(Lazy.force _refl_equal,[|typ;constr_of_term t|])) gls + let lr = constr_of_term t in + let typ = (* Termops.refresh_universes *) (pf_type_of gls lr) in + (app_global _refl_equal [|typ;constr_of_term t|] exact_check) gls end | 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 - let typ = Termops.refresh_universes (type_of t2) in - let prf = - mkApp(Lazy.force _trans_eq,[|typ;t1;t2;t3;_M 1;_M 2|]) in - Tacticals.New.tclTHENS (Proofview.V82.tactic (refine prf)) [(proof_tac p1);(proof_tac p2)] + let typ = (* Termops.refresh_universes *) (type_of t2) in + let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in + Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)] | Congr (p1,p2)-> let tf1=constr_of_term p1.p_lhs 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 - let typf = Termops.refresh_universes (type_of tf1) in - let typx = Termops.refresh_universes (type_of tx1) in - let typfx = Termops.refresh_universes (type_of (mkApp (tf1,[|tx1|]))) in + let typf = (* Termops.refresh_universes *)(type_of tf1) in + let typx = (* Termops.refresh_universes *) (type_of tx1) in + let typfx = (* Termops.refresh_universes *) (type_of (mkApp (tf1,[|tx1|]))) in let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in let lemma1 = - mkApp(Lazy.force _f_equal, - [|typf;typfx;appx1;tf1;tf2;_M 1|]) in + app_global _f_equal + [|typf;typfx;appx1;tf1;tf2;_M 1|] in let lemma2= - mkApp(Lazy.force _f_equal, - [|typx;typfx;tf2;tx1;tx2;_M 1|]) in + app_global _f_equal + [|typx;typfx;tf2;tx1;tx2;_M 1|] in let prf = - mkApp(Lazy.force _trans_eq, + app_global _trans_eq [|typfx; mkApp(tf1,[|tx1|]); mkApp(tf2,[|tx1|]); - mkApp(tf2,[|tx2|]);_M 2;_M 3|]) in - Tacticals.New.tclTHENS (Proofview.V82.tactic (refine prf)) - [Tacticals.New.tclTHEN (Proofview.V82.tactic (refine lemma1)) (proof_tac p1); + mkApp(tf2,[|tx2|]);_M 2;_M 3|] in + Tacticals.New.tclTHENS (Proofview.V82.tactic (prf refine)) + [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma1 refine)) (proof_tac p1); Tacticals.New.tclFIRST - [Tacticals.New.tclTHEN (Proofview.V82.tactic (refine lemma2)) (proof_tac p2); + [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2); reflexivity; Proofview.tclZERO (UserError ("Congruence" , (Pp.str @@ -305,46 +312,48 @@ let rec proof_tac p : unit Proofview.tactic = let ti=constr_of_term prf.p_lhs in let tj=constr_of_term prf.p_rhs in let default=constr_of_term p.p_lhs in - let intype = Termops.refresh_universes (type_of ti) in - let outtype = Termops.refresh_universes (type_of default) in + let intype = (* Termops.refresh_universes *) (type_of ti) in + let outtype = (* Termops.refresh_universes *) (type_of default) in let special=mkRel (1+nargs-argind) in let proj = Tacmach.New.of_old (build_projection intype outtype cstr special default) gl in let injt= - mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in - Tacticals.New.tclTHEN (Proofview.V82.tactic (refine injt)) (proof_tac prf) + app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in + Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end let refute_tac c t1 t2 p = Proofview.Goal.enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let intype = - Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt1)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt1)) gl in - let neweq= - mkApp(Lazy.force _eq, - [|intype;tt1;tt2|]) in + let neweq= new_app_global _eq [|intype;tt1;tt2|] in let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in let false_t=mkApp (c,[|mkVar hid|]) in - Tacticals.New.tclTHENS (assert_tac (Name hid) neweq) + Tacticals.New.tclTHENS (neweq (assert_tac (Name hid))) [proof_tac p; simplest_elim false_t] end +let refine_exact_check c gl = + let evm, _ = pf_apply e_type_of gl c in + Tacticals.tclTHEN (Refiner.tclEVARS evm) (exact_check c) gl + let convert_to_goal_tac c t1 t2 p = Proofview.Goal.enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let sort = - Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls tt2)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt2)) gl in - let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in + let neweq= new_app_global _eq [|sort;tt1;tt2|] in let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in let identity=mkLambda (Name x,sort,mkRel 1) in - let endt=mkApp (Lazy.force _eq_rect, - [|sort;tt1;identity;c;tt2;mkVar e|]) in - Tacticals.New.tclTHENS (assert_tac (Name e) neweq) - [proof_tac p; Proofview.V82.tactic (exact_check endt)] + let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in + Tacticals.New.tclTHENS (neweq (assert_tac (Name e))) + [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)] end let convert_to_hyp_tac c1 t1 c2 t2 p = @@ -357,29 +366,36 @@ let convert_to_hyp_tac c1 t1 c2 t2 p = simplest_elim false_t] end -let discriminate_tac cstr p = +let discriminate_tac (cstr,u as cstru) p = Proofview.Goal.enter begin fun gl -> let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in let intype = - Tacmach.New.of_old (fun gls -> Termops.refresh_universes (pf_type_of gls t1)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls t1)) gl in let concl = Proofview.Goal.concl gl in - let outsort = mkType (Termops.new_univ ()) in + (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in *) + (* let outsort = mkSort outsort in *) let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in - let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in - let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in - let trivial = Tacmach.New.of_old (fun gls -> pf_type_of gls identity) gl in - let outtype = mkType (Termops.new_univ ()) in + (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *) + (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *) + let identity = Universes.constr_of_global _I in + (* let trivial=pf_type_of gls identity in *) + let trivial = Universes.constr_of_global _True in + let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in + let outtype = mkSort outtype in let pred=mkLambda(Name xid,outtype,mkRel 1) in let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in - let proj = Tacmach.New.of_old (build_projection intype outtype cstr trivial concl) gl in - let injt=mkApp (Lazy.force _f_equal, - [|intype;outtype;proj;t1;t2;mkVar hid|]) in - let endt=mkApp (Lazy.force _eq_rect, - [|outtype;trivial;pred;identity;concl;injt|]) in - let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in - Tacticals.New.tclTHENS (assert_tac (Name hid) neweq) - [proof_tac p; Proofview.V82.tactic (exact_check endt)] + let proj = Tacmach.New.of_old (build_projection intype outtype 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=new_app_global _eq [|intype;t1;t2|] in + Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evm) + (Tacticals.New.tclTHENS (neweq (assert_tac (Name hid))) + [proof_tac p; Proofview.V82.tactic (endt exact_check)]) end (* wrap everything *) @@ -389,7 +405,7 @@ let build_term_to_complete uf meta pac = let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in let dummy_args = List.rev (List.init pac.arity meta) in let all_args = List.rev_append real_args dummy_args in - applistc (mkConstruct cinfo.ci_constr) all_args + applistc (mkConstructU cinfo.ci_constr) all_args let cc_tactic depth additionnal_terms = Proofview.Goal.enter begin fun gl -> @@ -457,7 +473,7 @@ let congruence_tac depth l = might be slow now, let's rather do something equivalent to a "simple apply refl_equal" *) -let simple_reflexivity () = apply (Lazy.force _refl_equal) +let simple_reflexivity () = apply (Universes.constr_of_global _refl_equal) (* The [f_equal] tactic. @@ -472,15 +488,17 @@ let f_equal = let type_of = Tacmach.New.pf_type_of gl in let cut_eq c1 c2 = try (* type_of can raise an exception *) - let ty = Termops.refresh_universes (type_of c1) in - Tacticals.New.tclTRY (Tacticals.New.tclTHEN - (Tactics.cut (mkApp (Lazy.force _eq, [|ty; c1; c2|]))) - (Tacticals.New.tclTRY (Proofview.V82.tactic (simple_reflexivity ())))) + let ty = (* Termops.refresh_universes *) (type_of c1) in + if eq_constr_nounivs c1 c2 then Proofview.tclUNIT () + else + Tacticals.New.tclTRY (Tacticals.New.tclTHEN + ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut) + (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) (fun c -> Proofview.V82.tactic (apply c))))) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE begin match kind_of_term concl with - | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) -> + | App (r,[|_;t;t'|]) when Globnames.is_global _eq r -> begin match kind_of_term t, kind_of_term t' with | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') -> let rec cuts i = diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli index a022a07da7..7c1d9f1c07 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -1,3 +1,4 @@ + (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) |