From d134b5afaf26a67149d999e95bd21b264b61429b Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 23 Oct 2003 19:05:52 +0000 Subject: 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 --- contrib/interface/centaur.ml4 | 4 ++-- contrib/interface/name_to_ast.ml | 4 ++-- contrib/interface/xlate.ml | 11 ++++++----- ide/coq.ml | 4 ++-- ide/coqide.ml | 4 ++-- library/decl_kinds.ml | 27 ++++++++++++--------------- toplevel/command.ml | 13 +------------ 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 -- cgit v1.2.3