diff options
| author | herbelin | 2002-10-23 23:02:09 +0000 |
|---|---|---|
| committer | herbelin | 2002-10-23 23:02:09 +0000 |
| commit | 8f995650ad67ac13a0806e9636795078c0aa4276 (patch) | |
| tree | 75502277b7ac94d957c73389294511e28d59c811 /contrib/interface | |
| parent | 85c65e07e70e7001b3048ea01c40b052da42293c (diff) | |
Clarification changements autour de Remark/Fact/Local
Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3180 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index ef7539bffd..7142f1e6d1 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1782,9 +1782,11 @@ let xlate_vernac = | VernacBeginSection id -> CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id)) | VernacEndSegment id -> CT_section_end (xlate_ident id) - | VernacStartTheoremProof (k, s, c, _, _) -> + | VernacStartTheoremProof (k, s, ([],c), _, _) -> CT_coerce_THEOREM_GOAL_to_COMMAND( CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,xlate_constr c)) + | VernacStartTheoremProof (k, s, (bl,c), _, _) -> + xlate_error "TODO: VernacStartTheoremProof" | VernacSuspend -> CT_suspend | VernacResume idopt -> CT_resume (xlate_ident_opt idopt) | VernacDefinition (k,s,ProveBody (bl,typ),_) -> |