Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé incomplètement prouvé comme axiome

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

4 files changed, 34 insertions, 11 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 78d2084373..743f1337af 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -80,6 +80,9 @@ let rec adjust_conclusion a cs = function
 
 (* 1| Constant definitions *)
 
+let definition_message id =
+  if_verbose message ((string_of_id id) ^ " is defined")
+
 let constant_entry_of_com (bl,com,comtypopt,opacity) =
   let sigma = Evd.empty in
   let env = Global.env() in
@@ -110,7 +113,7 @@ let declare_global_definition ident ce local =
   let (_,kn) = declare_constant ident (DefinitionEntry ce,IsDefinition) in
   if local = Local then
     msg_warning (pr_id ident ++ str" is declared as a global definition");
-  if_verbose message ((string_of_id ident) ^ " is defined");
+  definition_message ident;
   ConstRef kn
 
 let declare_definition ident local bl red_option c typopt hook =
@@ -123,7 +126,7 @@ let declare_definition ident local bl red_option c typopt hook =
         let c =
           SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type,false) in
         let _ = declare_variable ident (Lib.cwd(), c, IsDefinition) in
-        if_verbose message ((string_of_id ident) ^ " is defined");
+        definition_message ident;
         if Pfedit.refining () then 
           msgerrnl (str"Warning: Local definition " ++ pr_id ident ++ 
           str" is not visible from current goals");
@@ -178,14 +181,15 @@ let non_type_eliminations =
 let declare_one_elimination ind =
   let (mib,mip) = Global.lookup_inductive ind in 
   let mindstr = string_of_id mip.mind_typename in
-  let declare na c t =
-    let kn = Declare.declare_constant (id_of_string na)
+  let declare s c t =
+    let id = id_of_string s in
+    let kn = Declare.declare_constant id
       (DefinitionEntry
         { const_entry_body = c;
           const_entry_type = t;
           const_entry_opaque = false }, 
        Decl_kinds.IsDefinition) in
-    Options.if_verbose ppnl (str na ++ str " is defined"); 
+    definition_message id;
     kn
   in
   let env = Global.env () in
@@ -655,7 +659,7 @@ let save id const kind hook =
 	(Global, ConstRef kn) in
   hook l r;
   Pfedit.delete_current_proof ();
-  if_verbose message ((string_of_id id) ^ " is defined")
+  definition_message id
 
 let save_named opacity =
   let id,(const,persistence,hook) = Pfedit.cook_proof () in
@@ -682,6 +686,15 @@ let save_anonymous_with_strength kind opacity save_ident =
   (* we consider that non opaque behaves as local for discharge *)
   save save_ident const (IsGlobal (Proof kind)) hook
 
+let admit () =
+  let (id,k,typ,hook) = Pfedit.current_proof_statement () in
+  if k <> IsGlobal (Proof Conjecture) then
+    error "Only statements declared as conjecture can be admitted";
+  let (_,kn) = declare_constant id (ParameterEntry typ, IsConjecture) in
+  hook Global (ConstRef kn);
+  Pfedit.delete_current_proof ();
+  assumption_message id
+
 let get_current_context () =
   try Pfedit.get_current_goal_context ()
   with e when Logic.catchable_exception e -> 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 525ca0f18c..c12a494850 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -74,6 +74,10 @@ val save_anonymous : bool -> identifier -> unit
 
 val save_anonymous_with_strength : theorem_kind -> bool -> identifier -> unit
 
+(* [admit ()] aborts the current goal and save it as an assmumption *)
+
+val admit : unit -> unit
+
 (* [get_current_context ()] returns the evar context and env of the
    current open proof if any, otherwise returns the empty evar context
    and the current global env *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 0cb0b54e12..6665af74c2 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -308,9 +308,11 @@ let vernac_start_proof kind sopt (bl,t) lettop hook =
       (str "Proof editing mode not supported in module types");
   start_proof_and_print sopt (IsGlobal (Proof kind)) (bl,t) hook
 
-let vernac_end_proof is_opaque idopt =
-  if_verbose show_script ();
-  match idopt with
+let vernac_end_proof = function
+  | Admitted -> admit ()
+  | Proved (is_opaque,idopt) ->
+    if_verbose show_script ();
+    match idopt with
     | None -> save_named is_opaque
     | Some (id,None) -> save_anonymous is_opaque id
     | Some (id,Some kind) -> save_anonymous_with_strength kind is_opaque id
@@ -1119,7 +1121,7 @@ let interp c = match c with
   | VernacDefinition (k,id,d,f,_) -> vernac_definition k id d f
   | VernacStartTheoremProof (k,id,t,top,f) ->
       vernac_start_proof k (Some id) t top f
-  | VernacEndProof (opaq,idopt) -> vernac_end_proof opaq idopt
+  | VernacEndProof e -> vernac_end_proof e
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,l) -> vernac_assumption stre l
   | VernacInductive (finite,l) -> vernac_inductive finite l
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index aa307203fe..5f3ff5444b 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -142,6 +142,10 @@ type local_decl_expr =
 
 type module_binder = identifier list * module_type_ast
 
+type proof_end =
+  | Admitted
+  | Proved of opacity_flag * (identifier * theorem_kind option) option
+
 type vernac_expr =
   (* Control *)
   | VernacList of located_vernac_expr list
@@ -175,7 +179,7 @@ type vernac_expr =
       declaration_hook * definitionkind
   | VernacStartTheoremProof of theorem_kind * identifier *
       (local_binder list * constr_expr) * bool * declaration_hook
-  | VernacEndProof of opacity_flag * (identifier * theorem_kind option) option
+  | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
   | VernacAssumption of assumption_kind * simple_binder with_coercion list
   | VernacInductive of inductive_flag * inductive_expr list