diff options
| author | herbelin | 2009-11-27 19:48:59 +0000 |
|---|---|---|
| committer | herbelin | 2009-11-27 19:48:59 +0000 |
| commit | 93a5f1e03e29e375be69a2361ffd6323f5300f86 (patch) | |
| tree | 713b89aeac45df6b697d5b2a928c5808bb72d9fd /plugins/interface | |
| parent | 82d94b8af248edcd14d737ec005d560ecf0ee9e0 (diff) | |
Added support for definition of fixpoints using tactics.
Fixed some bugs in -beautify and robustness of {struct} clause.
Note: I tried to make the Automatic Introduction mode on by default
for version >= 8.3 but it is to complicated to adapt even in the
standard library.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12546 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/interface')
| -rw-r--r-- | plugins/interface/xlate.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index 9ba1d6715c..5f3b6b28d4 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -1917,7 +1917,7 @@ let rec 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, [Some (_,s), (bl,c)], _, _) -> + | VernacStartTheoremProof (k, [Some (_,s), (bl,c,None)], _, _) -> CT_coerce_THEOREM_GOAL_to_COMMAND( CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s, xlate_binder_list bl, xlate_formula c)) @@ -1993,9 +1993,10 @@ let rec xlate_vernac = | VernacFixpoint ([],_) -> xlate_error "mutual recursive" | VernacFixpoint ((lm :: lmi),boxed) -> let strip_mutrec (((_,fid), (n, ro), bl, arf, ardef), _ntn) = + if ardef = None then xlate_error "Fixpoint proved by tactics"; let struct_arg = make_fix_struct (n, bl) in let arf = xlate_formula arf in - let ardef = xlate_formula ardef in + let ardef = xlate_formula (Option.get ardef) in match xlate_binder_list bl with | CT_binder_list (b :: bl) -> CT_fix_rec (xlate_ident fid, CT_binder_ne_list (b, bl), @@ -2006,8 +2007,9 @@ let rec xlate_vernac = | VernacCoFixpoint ([],boxed) -> xlate_error "mutual corecursive" | VernacCoFixpoint ((lm :: lmi),boxed) -> let strip_mutcorec (((_,fid), bl, arf, ardef), _ntn) = + if ardef = None then xlate_error "Fixpoint proved by tactics"; CT_cofix_rec (xlate_ident fid, xlate_binder_list bl, - xlate_formula arf, xlate_formula ardef) in + xlate_formula arf, xlate_formula (Option.get ardef)) in CT_cofix_decl (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)) | VernacScheme [] -> xlate_error "induction scheme" |