From 21c8f5d0b74e72f61a086d92660d25ce35c482b7 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 16 Jun 2008 10:17:13 +0000
Subject: Add possibility to match on defined hypotheses, using brackets to
 disambiguate syntax: [ H := [ ?x ] : context C [ foo ] |- _ ] is ok, as well
 as [ H := ?x : nat |- _ ] or [H := foo |- _ ], but [ H := ?x : context C [
 foo ] ] will not parse. Add applicative contexts in tactics match, to be able
 to match arbitrary partial applications, e.g.: match f 0 1 2 with appcontext
 C [ f ?x ] => ... end will bind C to [ ∙ 1 2 ] and x to 0. Minor improvements
 in coqdoc.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11129 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tools/coqdoc/output.ml  | 2 +-
 tools/coqdoc/pretty.mll | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'tools')

diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 009e4dd11a..067af63f2b 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -66,7 +66,7 @@ let is_tactic =
       "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by";
       "reflexivity"; "symmetry"; "transitivity";
       "replace"; "setoid_replace"; "inversion"; "inversion_clear";
-      "pattern"; "intuition"; "congruence";
+      "pattern"; "intuition"; "congruence"; "fail"; "fresh";
       "trivial"; "exact"; "tauto"; "firstorder"; "ring";
       "clapply"; "program_simpl"; "eapply"; "auto"; "eauto" ]
 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index d5d8702bcc..36ed0472b2 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -170,11 +170,12 @@ let firstchar =
   ['A'-'Z' 'a'-'z' '_' 
   (* iso 8859-1 accents *) 
   '\192'-'\214' '\216'-'\246' '\248'-'\255' ] |
+  (* *)
   '\194' '\185' |
   (* utf-8 latin 1 supplement *) 
   '\195' ['\128'-'\191'] |
   (* utf-8 letterlike symbols *) 
-  '\206' ['\177'-'\183'] |
+  '\206' ('\160' | [ '\177'-'\183'] | '\187') |
   '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
     | '\129' [ '\176'-'\187' ] (* superscripts *)
     | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
-- 
cgit v1.2.3