Fix bug #3698: stack overflow due to eta+canonical structures in

unification.

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