diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2017-05-29 17:02:45 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2017-05-29 17:02:45 +0200 |
commit | 7855fa596d5308a1c153b98146e57e9408bf8c5d (patch) | |
tree | 26be526fce869411ee678aed207c75467e4cf34b | |
parent | e95d1717c20b12234133e433d34d9457c4332942 (diff) |
Equality cleanup: remove constr_of_global
-rw-r--r-- | plugins/cc/cctac.ml | 9 | ||||
-rw-r--r-- | tactics/equality.ml | 36 | ||||
-rw-r--r-- | tactics/equality.mli | 2 |
3 files changed, 27 insertions, 20 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index b3017f359..43c06a54d 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -231,9 +231,9 @@ let make_prb gls depth additionnal_terms = let build_projection intype (cstr:pconstructor) special default gls= let open Tacmach.New in let ci= (snd(fst cstr)) in - let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in + let sigma, body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in let id=pf_get_new_id (Id.of_string "t") gls in - mkLambda(Name id,intype,body) + sigma, mkLambda(Name id,intype,body) (* generate an adhoc tactic following the proof tree *) @@ -346,12 +346,13 @@ let rec proof_tac p : unit Proofview.tactic = let special=mkRel (1+nargs-argind) in refresh_universes (type_of ti) (fun intype -> refresh_universes (type_of default) (fun outtype -> - let proj = + let sigma, proj = build_projection intype cstr special default gl in let injt= app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in - Tacticals.New.tclTHEN injt (proof_tac prf))) + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Tacticals.New.tclTHEN injt (proof_tac prf)))) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end } diff --git a/tactics/equality.ml b/tactics/equality.ml index e6278943d..b48d60a4f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -874,7 +874,7 @@ let descend_then env sigma head dirn = let dirn_env = Environ.push_rel_context cstr.(dirn-1).cs_args env in (dirn_nlams, dirn_env, - (fun dirnval (dfltval,resty) -> + (fun sigma dirnval (dfltval,resty) -> let deparsign = make_arity_signature env sigma true indf in let p = it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in @@ -887,7 +887,7 @@ let descend_then env sigma head dirn = List.map build_branch (List.interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in - Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl))) + sigma, Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl))) (* Now we need to construct the discriminator, given a discriminable position. This boils down to: @@ -932,23 +932,28 @@ let build_selector env sigma dirn c ind special default = let brl = List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in - mkCase (ci, p, c, Array.of_list brl) + sigma, mkCase (ci, p, c, Array.of_list brl) -let build_coq_False () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ()) -let build_coq_True () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_True ()) -let build_coq_I () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_I ()) +let new_global sigma gr = + let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr + in Sigma.to_evar_map sigma, c + +let build_coq_False sigma = new_global sigma (build_coq_False ()) +let build_coq_True sigma = new_global sigma (build_coq_True ()) +let build_coq_I sigma = new_global sigma (build_coq_I ()) let rec build_discriminator env sigma dirn c = function | [] -> let ind = get_type_of env sigma c in - let true_0,false_0 = - build_coq_True(),build_coq_False() in + let sigma, true_0 = build_coq_True sigma in + let sigma, false_0 = build_coq_False sigma in build_selector env sigma dirn c ind true_0 false_0 | ((sp,cnum),argnum)::l -> + let sigma, false_0 = build_coq_False sigma in let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in - let subval = build_discriminator cnum_env sigma dirn newc l in - kont subval (build_coq_False (),mkSort (Prop Null)) + let sigma, subval = build_discriminator cnum_env sigma dirn newc l in + kont sigma subval (false_0,mkSort (Prop Null)) (* Note: discrimination could be more clever: if some elimination is not allowed because of a large impredicative constructor in the @@ -991,9 +996,9 @@ let ind_scheme_of_eq lbeq = let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq = - let i = build_coq_I () in - let absurd_term = build_coq_False () in - let eq_elim, eff = ind_scheme_of_eq lbeq in + let sigma, i = build_coq_I sigma in + let sigma, absurd_term = build_coq_False sigma in + let eq_elim, eff = ind_scheme_of_eq lbeq in let sigma, eq_elim = Evd.fresh_global (Global.env ()) sigma eq_elim in let eq_elim = EConstr.of_constr eq_elim in sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term), @@ -1013,7 +1018,7 @@ let apply_on_clause (f,t) clause = let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = let e = next_ident_away eq_baseid (ids_of_context env) in let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in - let discriminator = + let sigma, discriminator = build_discriminator e_env sigma dirn (mkVar e) cpath in let sigma,(pf, absurd_term), eff = discrimination_pf env sigma e (t,t1,t2) discriminator lbeq in @@ -1309,7 +1314,8 @@ let rec build_injrec env sigma dflt c = function let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in let sigma, (subval,tuplety,dfltval) = build_injrec cnum_env sigma dflt newc l in - sigma, (kont subval (dfltval,tuplety), tuplety,dfltval) + let sigma, res = kont sigma subval (dfltval,tuplety) in + sigma, (res, tuplety,dfltval) with UserError _ -> failwith "caught" diff --git a/tactics/equality.mli b/tactics/equality.mli index b47be3bbc..27be5affb 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -126,4 +126,4 @@ val set_eq_dec_scheme_kind : mutual scheme_kind -> unit (* [build_selector env sigma i c t u v] matches on [c] of type [t] and returns [u] in branch [i] and [v] on other branches *) val build_selector : env -> evar_map -> int -> constr -> types -> - constr -> constr -> constr + constr -> constr -> evar_map * constr |