diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 39 |
1 files changed, 0 insertions, 39 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e9fbf6d15..3d25e7607 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4134,45 +4134,6 @@ let admit_as_an_axiom = simplest_case (Coqlib.build_coq_proof_admitted ()) <*> Proofview.mark_as_unsafe -(* let current_sign = Global.named_context() *) -(* and global_sign = pf_hyps gl in *) -(* let poly = Flags.is_universe_polymorphism () in (\*FIXME*\) *) -(* let sign,secsign = *) -(* List.fold_right *) -(* (fun (id,_,_ as d) (s1,s2) -> *) -(* if mem_named_context id current_sign & *) -(* interpretable_as_section_decl (Context.lookup_named id current_sign) d *) -(* then (s1,add_named_decl d s2) *) -(* else (add_named_decl d s1,s2)) *) -(* global_sign (empty_named_context,empty_named_context) in *) -(* let name = add_suffix (get_current_proof_name ()) "_admitted" in *) -(* let na = next_global_ident_away name (pf_ids_of_hyps gl) in *) -(* let evd, nf = nf_evars_and_universes (project gl) in *) -(* let ctx = Evd.universe_context evd in *) -(* let newconcl = nf (pf_concl gl) in *) -(* let newsign = Context.map_named_context nf sign in *) -(* let concl = it_mkNamedProd_or_LetIn newconcl newsign in *) -(* if occur_existential concl then error"\"admit\" cannot handle existentials."; *) -(* let entry = *) -(* (Pfedit.get_used_variables(),poly,(concl,ctx),None) *) -(* in *) -(* let cd = Entries.ParameterEntry entry in *) -(* let decl = (cd, IsAssumption Logical) in *) -(* (\** ppedrot: seems legit to have admitted subproofs as local*\) *) -(* let con = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true na decl in *) -(* let evd, axiom = evd, (mkConstU (con, Univ.UContext.instance ctx)) in *) -(* (\* let evd, axiom = Evd.fresh_global (pf_env gl) (project gl) (ConstRef con) in *\) *) -(* let gl = tclTHEN (tclEVARS evd) *) -(* (tclTHEN (convert_concl_no_check newconcl DEFAULTcast) *) -(* (exact_check *) -(* (applist (axiom, *) -(* List.rev (Array.to_list (instance_from_named_context sign)))))) *) -(* gl *) -(* in *) -(* Pp.feedback Interface.AddedAxiom; *) -(* gl *) -(* >>>>>>> .merge_file_iUuzZK *) - let unify ?(state=full_transparent_state) x y = Proofview.Goal.nf_enter begin fun gl -> try |