diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-23 19:10:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-23 19:10:58 +0000 |
| commit | 64921b7e96c081f1d9d39ffe636bd34bc0129200 (patch) | |
| tree | 9fe907069a6a07321435aa28296b3ee3a0c267b3 /parsing/g_vernac.ml4 | |
| parent | 1b8b3e43a07359be94dc3fcfd41acb8394ccd8d3 (diff) | |
Conjecture declare maintenant un axiome; reorganisation VernacDefinition
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4713 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 0c79c9973..a6d9c2420 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -108,20 +108,21 @@ GEXTEND Gram [ [ "Theorem" -> Theorem | IDENT "Lemma" -> Lemma | IDENT "Fact" -> Fact - | IDENT "Remark" -> Remark - | IDENT "Conjecture" -> Conjecture ] ] + | IDENT "Remark" -> Remark ] ] ; def_token: - [ [ "Definition" -> (fun _ _ -> ()), Global, GDefinition - | IDENT "Local" -> (fun _ _ -> ()), Local, LDefinition - | IDENT "SubClass" -> Class.add_subclass_hook, Global, GSubClass - | IDENT "Local"; IDENT "SubClass" -> Class.add_subclass_hook, Local, LSubClass ] ] + [ [ "Definition" -> (fun _ _ -> ()), (Global, Definition) + | IDENT "Local" -> (fun _ _ -> ()), (Local, Definition) + | IDENT "SubClass" -> Class.add_subclass_hook, (Global, SubClass) + | IDENT "Local"; IDENT "SubClass" -> + Class.add_subclass_hook, (Local, SubClass) ] ] ; assumption_token: [ [ "Hypothesis" -> (Local, Logical) | "Variable" -> (Local, Definitional) | "Axiom" -> (Global, Logical) - | "Parameter" -> (Global, Definitional) ] ] + | "Parameter" -> (Global, Definitional) + | IDENT "Conjecture" -> (Global,Conjectural) ] ] ; assumptions_token: [ [ IDENT "Hypotheses" -> (Local, Logical) @@ -192,8 +193,8 @@ GEXTEND Gram (* Definition, Theorem, Variable, Axiom, ... *) [ [ thm = thm_token; id = base_ident; ":"; c = constr -> VernacStartTheoremProof (thm, id, ([], c), false, (fun _ _ -> ())) - | (f,d,e) = def_token; id = base_ident; b = def_body -> - VernacDefinition (d, id, b, f, e) + | (f,d) = def_token; id = base_ident; b = def_body -> + VernacDefinition (d, id, b, f) | stre = assumption_token; bl = ne_params_list -> VernacAssumption (stre, bl) | stre = assumptions_token; bl = ne_params_list -> @@ -385,17 +386,18 @@ GEXTEND Gram VernacCanonical qid | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> let s = Ast.coerce_global_to_id qid in - VernacDefinition (Global,s,d,Recordobj.add_object_hook,SCanonical) + VernacDefinition + ((Global,CanonicalStructure),s,d,Recordobj.add_object_hook) (* Rem: LOBJECT, OBJCOERCION, LOBJCOERCION have been removed (they were unused and undocumented) *) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> let s = Ast.coerce_global_to_id qid in - VernacDefinition (Global,s,d,Class.add_coercion_hook,GCoercion) + VernacDefinition ((Global,Coercion),s,d,Class.add_coercion_hook) | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body -> let s = Ast.coerce_global_to_id qid in - VernacDefinition (Local,s,d,Class.add_coercion_hook,LCoercion) + VernacDefinition ((Local,Coercion),s,d,Class.add_coercion_hook) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = base_ident; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (Local, f, s, t) |