Portage (pour la forme) de minicoq

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@360 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 3 deletions

diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index ae26e3f3c..bf75cdd38 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -84,9 +84,14 @@ EXTEND
 	end
     | "("; c = term; "::"; t = term; ")" ->
 	DOP2 (Cast, c, t)
-    | "<"; p = term; ">"; IDENT "Case"; c = term; "of"; 
-      bl = LIST0 term; "end" ->
-	DOPN (MutCase None, Array.of_list (p :: c :: bl))
+    | "<"; p = term; ">"; 
+	IDENT "Case"; c = term; ":"; "Ind"; id = IDENT; i = INT;
+	"of"; bl = LIST0 term; "end" ->
+	  let ind = (path_of_string id,int_of_string i) in
+	  let nc = List.length bl in
+	  let dummy_pats = Array.create nc RegularPat in
+	  let dummy_ci = [||],(ind,[||],nc,None,dummy_pats) in
+	  DOPN (MutCase dummy_ci, Array.of_list (p :: c :: bl))
   ] ];
   command: 
   [ [ "Definition"; id = IDENT; ":="; c = term; "." ->