From d4e696cb8145701356fb9993a8a97e970e83ff8c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Jun 2008 14:57:51 +0000
Subject: 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
---
 tactics/tactics.ml | 19 -------------------
 1 file changed, 19 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c992fcc2ab..905511b120 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
-*)
-- 
cgit v1.2.3