diff options
| author | notin | 2006-10-04 13:05:58 +0000 |
|---|---|---|
| committer | notin | 2006-10-04 13:05:58 +0000 |
| commit | 79fba16cf02b83ac2b4866e582dd4481314770b4 (patch) | |
| tree | a6f268fe0edc8811bc8222c46503aa828da885eb | |
| parent | 75862b96afd73704bc56f52ef2375d128ad53150 (diff) | |
Correction bug #1204 + maj CHANGES
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9204 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | tools/coqdoc/index.mll | 1 | ||||
| -rw-r--r-- | tools/coqdoc/pretty.mll | 23 |
3 files changed, 16 insertions, 10 deletions
@@ -12,6 +12,8 @@ Changes from V8.1beta to V8.1 infer the predicate in "(exist _ 0 (refl_equal 0) : {n:nat | n=0 })") - Support for "where" clause in cofixpoint definitions - Support for argument lists of arbitrary length in Tactic Notation +- [rewrite ... in H] now fails if [H] is used either in an hypohesis + or in the goal Changes from V8.0 to V8.1beta ============================= diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index 5278945ef5..4e54044473 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -364,6 +364,7 @@ and end_ident = parse and module_ident = parse | space+ { module_ident lexbuf } + | '"' { string lexbuf; module_ident lexbuf } | ident space* ":=" { () } | ident diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 2de6838ea5..869df4eef6 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -398,19 +398,22 @@ and coq = parse { () } | gallina_kw_to_hide { let s = lexeme lexbuf in - if !light && section_or_end s then begin - let eol = skip_to_dot lexbuf in - if eol then coq_bol lexbuf else coq lexbuf - end else begin - ident s (lexeme_start lexbuf); - let eol=body lexbuf in - if eol then coq_bol lexbuf else coq lexbuf - end } + if !light && section_or_end s then + begin + let eol = skip_to_dot lexbuf in + if eol then coq_bol lexbuf else coq lexbuf + end + else + begin + ident s (lexeme_start lexbuf); + let eol=body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf + end } | gallina_kw { let s = lexeme lexbuf in ident s (lexeme_start lexbuf); - let eol = body lexbuf in - if eol then coq_bol lexbuf else coq lexbuf } + let eol = body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } | space+ { char ' '; coq lexbuf } | eof { () } |