From 93a5f1e03e29e375be69a2361ffd6323f5300f86 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 27 Nov 2009 19:48:59 +0000
Subject: 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
---
 plugins/interface/xlate.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'plugins/interface')

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"
-- 
cgit v1.2.3