Conjecture declare maintenant un axiome; reorganisation VernacDefinition

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

7 files changed, 27 insertions, 40 deletions

diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 4290eca61..f4a8580eb 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -551,8 +551,8 @@ let solve_hook n =
 let abort_hook s = output_results_nl (ctf_AbortedMessage !global_request_id s)
 
 let interp_search_about_item = function
-  | SearchRef qid -> SearchRef (Nametab.global qid)
-  | SearchString s as x -> x
+  | SearchRef qid -> GlobSearchRef (Nametab.global qid)
+  | SearchString s -> GlobSearchString s
 
 let pcoq_search s l =
   ctv_SEARCH_LIST:=[];
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 6e44f2b11..cdf83b22b 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -159,9 +159,9 @@ let make_variable_ast name typ implicits =
     
 
 let make_definition_ast name c typ implicits =
-  VernacDefinition (Global, name, DefineBody ([], None,
+  VernacDefinition ((Global,Definition), name, DefineBody ([], None,
     (constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
-    (fun _ _ -> ()),GDefinition)
+    (fun _ _ -> ()))
   ::(implicits_to_ast_list implicits);;
 
 (* This function is inspired by print_constant *)
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index c3355b61b..9a0ecced4 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1184,8 +1184,7 @@ let xlate_thm x = CT_thm (match x with
   | Theorem -> "Theorem"
   | Remark -> "Remark"
   | Lemma -> "Lemma"
-  | Fact -> "Fact"
-  | Conjecture -> "Conjecture")
+  | Fact -> "Fact")
 
 
 let xlate_defn x = CT_defn (match x with
@@ -1196,7 +1195,9 @@ let xlate_var x = CT_var (match x with
  | (Global,Definitional) -> "Parameter"
  | (Global,Logical) -> "Axiom"
  | (Local,Definitional) -> "Variable"
- | (Local,Logical) -> "Hypothesis");;
+ | (Local,Logical) -> "Hypothesis"
+ | (Global,Conjectural) -> "Conjecture"
+ | (Local,Conjectural) -> xlate_error "No local conjecture");;
 
 
 let xlate_dep =
@@ -1472,11 +1473,11 @@ let xlate_vernac =
       xlate_error "TODO: VernacStartTheoremProof"
   | VernacSuspend -> CT_suspend
   | VernacResume idopt -> CT_resume (xlate_ident_opt (option_app snd idopt))
-  | VernacDefinition (k,s,ProveBody (bl,typ),_,_) ->
+  | VernacDefinition ((k,_),s,ProveBody (bl,typ),_) ->
       if bl <> [] then xlate_error "TODO: Def bindings";
       CT_coerce_THEOREM_GOAL_to_COMMAND(
 	CT_theorem_goal (CT_coerce_DEFN_to_DEFN_OR_THM (xlate_defn k), xlate_ident s,xlate_formula typ))
-  | VernacDefinition (kind,s,DefineBody(bl,red_option,c,typ_opt),_,_) ->
+  | VernacDefinition ((kind,_),s,DefineBody(bl,red_option,c,typ_opt),_) ->
       CT_definition
 	(xlate_defn kind, xlate_ident s, xlate_binder_list bl,
 	   cvt_optional_eval_for_definition c red_option,
diff --git a/ide/coq.ml b/ide/coq.ml
index 487bc13a6..1f0efbe71 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -286,7 +286,7 @@ let word_class s =
 type reset_info = NoReset | Reset of Names.identifier * bool ref
 
 let compute_reset_info = function 
-  | VernacDefinition (_, id, DefineBody _, _, _) 
+  | VernacDefinition (_, id, DefineBody _, _) 
   | VernacBeginSection id 
   | VernacDefineModule (id, _, _, _) 
   | VernacDeclareModule (id, _, _, _)
@@ -294,7 +294,7 @@ let compute_reset_info = function
   | VernacAssumption (_, (_,(id,_))::_)
   | VernacInductive (_, (id,_,_,_,_) :: _) ->
       Reset (id, ref true)
-  | VernacDefinition (_, id, ProveBody _, _, _)
+  | VernacDefinition (_, id, ProveBody _, _)
   | VernacStartTheoremProof (_, id, _, _, _) ->
       Reset (id, ref false)
   | _ -> NoReset
diff --git a/ide/coqide.ml b/ide/coqide.ml
index ae04c8d64..13d916480 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -499,7 +499,7 @@ let is_empty () = Stack.is_empty processed_stack
 
 let update_on_end_of_proof id =
   let lookup_lemma = function
-  | { ast = _, ( VernacDefinition (_, _, ProveBody _, _, _)
+  | { ast = _, ( VernacDefinition (_, _, ProveBody _, _)
 	       | VernacDeclareTacticDefinition _
 	       | VernacStartTheoremProof _) ; 
       reset_info = Reset (_, r) } -> 
@@ -1316,7 +1316,7 @@ Please restart and report NOW.";
 	  | { ast = _, ( VernacStartTheoremProof _ 
 		       | VernacGoal _
 		       | VernacDeclareTacticDefinition _
-		       | VernacDefinition (_,_,ProveBody _,_,_));
+		       | VernacDefinition (_,_,ProveBody _,_));
 	      reset_info=Reset(id,{contents=false})} ->
 	      ignore (pop ());
 	      (try 
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index a47fb9086..74e256684 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -10,6 +10,10 @@
 
 (* Informal mathematical status of declarations *)
 
+type locality_flag = (*bool (* local = true; global = false *)*)
+  | Local
+  | Global
+
 (* Kinds used at parsing time *)
 
 type theorem_kind =
@@ -17,24 +21,16 @@ type theorem_kind =
   | Lemma
   | Fact
   | Remark
-  | Conjecture
 
-type definitionkind =
-  | LDefinition
-  | GDefinition
-  | LCoercion
-  | GCoercion
-  | LSubClass
-  | GSubClass
-  | SCanonical
-
-type locality_flag = (*bool (* local = true; global = false *)*)
-  | Local
-  | Global
+type definition_object_kind =
+  | Definition
+  | Coercion
+  | SubClass
+  | CanonicalStructure
 
 type strength = locality_flag (* For compatibility *)
 
-type type_as_formula_kind = Definitional | Logical
+type type_as_formula_kind = Definitional | Logical | Conjectural
 
 (* [assumption_kind] 
 
@@ -42,10 +38,11 @@ type type_as_formula_kind = Definitional | Logical
    ------------------------------------
    Definitional |  Variable   | Parameter
    Logical      |  Hypothesis | Axiom
+
 *)
 type assumption_kind = locality_flag * type_as_formula_kind
 
-type definition_kind = locality_flag
+type definition_kind = locality_flag * definition_object_kind
 
 (* Kinds used in proofs *)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 63b9f5dbf..57a187f13 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -116,7 +116,7 @@ let declare_global_definition ident ce local =
   definition_message ident;
   ConstRef kn
 
-let declare_definition ident local bl red_option c typopt hook =
+let declare_definition ident (local,_) bl red_option c typopt hook =
   let ce = constant_entry_of_com (bl,c,typopt,false) in
   if bl<>[] && red_option <> None then 
     error "Evaluation under a local context not supported";
@@ -630,16 +630,6 @@ let start_proof_com sopt kind (bl,t) hook =
   let _ = Typeops.infer_type env c in
   start_proof id kind c hook
 
-(*
-let apply_tac_not_declare id pft = function
-  | None -> error "Type of Let missing"
-  | Some typ ->
-    let cutt = Hiddentac.h_cut typ
-    and exat = Hiddentac.h_exact pft in
-    Pfedit.delete_current_proof ();
-    Pfedit.by (Refiner.tclTHENSV cutt [|introduction id;exat|])
-*)
-
 let save id const kind hook =
   let {const_entry_body = pft;
        const_entry_type = tpo;
@@ -658,7 +648,6 @@ let save id const kind hook =
         let _,kn = declare_constant id (DefinitionEntry const, k) in
 	(Global, ConstRef kn) in
   hook l r;
-  if kind = IsGlobal (Proof Conjecture) then warning "Proved conjecture";
   Pfedit.delete_current_proof ();
   definition_message id