Backtrack sur l'"optimisation" de admit (révision 11084). Comme le

fait remarquer Bruno, c'est ne pas anodin de laisser croire qu'on
admet une conjecture alors qu'on admet uniquement la conclusion de
cette conjecture, conclusion qui peut être incohérente et qui ne le
serait pas si on avait gardé le contexte du but.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11089 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 19 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c992fcc2a..905511b12 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2885,24 +2885,6 @@ let tclABSTRACT name_op tac gl =
 
 
 let admit_as_an_axiom gl =
-  let ccl = pf_concl gl in
-  let ids_of_sign = pf_ids_of_hyps gl in
-  let vars = global_vars_set (Global.env ()) ccl in
-  let sign = List.filter (fun (id,_,_) -> Idset.mem id vars) (pf_hyps gl) in
-  let name = add_suffix (get_current_proof_name ()) "_admitted" in
-  let na = next_global_ident_away false name ids_of_sign in
-  let concl = it_mkNamedProd_or_LetIn ccl sign in
-  if occur_existential concl then error "\"admit\" cannot handle existentials";
-  let axiom =
-    let cd = Entries.ParameterEntry (concl,false) in
-    let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in
-    constr_of_global (ConstRef con)
-  in
-  exact_no_check 
-    (applist (axiom, 
-              List.rev (Array.to_list (instance_from_named_context sign))))
-    gl
-(*
   let current_sign = Global.named_context()
   and global_sign = pf_hyps gl in
   let sign,secsign = 
@@ -2926,4 +2908,3 @@ let admit_as_an_axiom gl =
     (applist (axiom, 
               List.rev (Array.to_list (instance_from_named_context sign))))
     gl
-*)