From 0cc6076e7d4d92c1d899d450b2336dadbeb5f1b1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 25 Apr 2008 18:07:44 +0000
Subject: Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve
 des théorèmes prouvés par récursion ou corécursion mutuelle.

Correction au passage du parsing et du printing des tactiques
fix/cofix et documentation de ces tactiques.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coq.ml        | 2 +-
 ide/highlight.mll | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'ide')

diff --git a/ide/coq.ml b/ide/coq.ml
index 128717acf4..e75f507210 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -351,7 +351,7 @@ let compute_reset_info = function
   | VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
       Reset (id, ref true)
   | VernacDefinition (_, (_,id), ProveBody _, _)
-  | VernacStartTheoremProof (_, (_,id), _, _, _) ->
+  | VernacStartTheoremProof (_, [Some (_,id), _], _, _) ->
       Reset (id, ref false)
   | _ -> NoReset
 
diff --git a/ide/highlight.mll b/ide/highlight.mll
index c033a6af5e..79b4e25aa7 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -82,7 +82,7 @@ rule next_order = parse
       { comment_start := lexeme_start lexbuf; comment lexbuf }
   | "Module Type"
       { lexeme_start lexbuf, lexeme_end lexbuf, "kwd" }
-  | "Program" space+ ident as id { lexeme_start lexbuf, lexeme_end lexbuf, "decl" }
+  | "Program" space+ ident { lexeme_start lexbuf, lexeme_end lexbuf, "decl" }
   | ident as id 
       { if is_keyword id then 
 	    lexeme_start lexbuf, lexeme_end lexbuf, "kwd" 
-- 
cgit v1.2.3