| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
| |
(it interfered badly with utf-8: just take an utf-8 like "forall" which
starts in iso-8859-1 with a "a circonflex"; nothing is lost since
intentedly iso-8859-1 chars can only occur in comments and there is no
ident detection in comments)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12895 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
- Local Definitions were considered Global Definitions in globalization file
(bug #2288) [I made them "var" which makes them indexed like
Variables, should we have an extra category just for Let's?]
- the syntax of "[[" was not properly enforced in parse-comments mode
- improved documentation of a few vernac file of the library
- fixed a bug in Makefile.doc leading to build a bigger and bigger
Library.pdf file
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12894 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
from a incorrect computation of logical names + bug in rendering of
name-based notations, aka abbreviations or syntactic definitions).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12893 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
ide/proof
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12892 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
- A more clever strategy than the use of null spaces (in revision 12058)
for collapsing multi-byte utf-8 characters into one character
(toplevel.ml, 8.3 and trunk only)
- Fixing discard_to_dot in the presence of iterated lexing failures
- Made the lexer state aligned with the start of utf-8 chars instead
of staying in the middle of multi-byte chars when a token is not
recognized (lexer.ml4)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12891 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- make links to section variables working (used qualified names for
disambiguation and fixed the place in intern_var where to dump them)
(wish #2277)
- mapping of physical to logical paths now follows coq (see bug #2274)
(incidentally, it was also incorrectly seeing foobar.v as a in directory foo)
- added links for notations
- added new category "other" for indexing entries not starting with latin letter
(e.g. notations or non-latin identifiers which was otherwise broken)
- protected non-notation strings (from String.v) from utf8 symbol interpretation
- incidentally quoted parseable _ in notations to avoid confusion with
placeholder in the "_ + _" form of notation
- improved several "Sys_error" error messages
- fixed old bug about second dot of ".." being interpreted as regular dot
- removed obsolete lexer in index.mll (and renamed index.mll to index.ml)
- added a test-suite file for testing various features of coqdoc
Things that still do not work:
- when a notation is redefined several times in the same scope, only
the link to the first definition works
- if chars and symbols are not separated in advance, idents
that immediately follow symbols are not detected
(e.g. as in {True}+{True} where coqdoc sees a symbol "+{True}")
- parentheses, curly brackets and semi-colon not linked in notations
Things that can probably be improved:
- all notations are indexed in the same category "other"; can we do better?
- all non-latin identifiers (e.g. Greek letters) are also indexed in the
same "other" category; can we do better?
- globalization data for notations could be compacted (currently there is one
line per each proper location covered by the notation)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12890 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
inductive types (see bug report #2250).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12889 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12888 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12887 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
detect indirect dependencies).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12886 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
of a lemma was no longer done).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12885 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12883 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
(currently only one expansion but could be virtually made user-parametrizable).
Also fixed a bug in recursive notations happening with multiple-tokens
separators (see Notations.v in test-suite).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12881 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12880 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12879 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
all current goals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12878 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12877 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12876 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12875 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12874 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
qui empêchait la compilation de certaines contributions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12873 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12872 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
camlp4deps/use lines
The build error Y. Makarov recently reported on coq-club was caused by some
.ml4 having dos-style end-of-line in his source-tree, and hence \r appearing in
the camlp4o commandline. We now simply discard what appears after camlp4xxx "...".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12871 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12870 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12869 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
(Forgot the file in last commit).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12868 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
building a new goal evar defs.
Allow customization of the reduction function applied to subtac
obligations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12867 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12865 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
variables (which include let-ins in cstr type)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12864 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12862 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12861 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12860 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12859 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12858 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12857 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12856 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
destr_t, etc etc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12855 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12854 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
Fix minor bug in Program wellfounded definitions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12853 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12852 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
Fix a bug in dependent elimination when treating defined variables in
the context.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12851 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12850 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
informative exception if some constraints do not unify.
All calls except one used to raise a less informative exception when the
constraints weren't solved.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12849 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
- disallow dynamic generation of [case] constructs through [find_scheme]
during a rewrite, as it changes the global environment and subsequent
manipulations of the tactic may use an outdated environment.
- use local exception names so as not to catch and hide unexpected
[Not_found] exceptions.
- fix lifting of constraints for dependent function types
- Allow rewriting on morphisms (terms in function position) even with
[rewrite] (fixes bug #2178).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12848 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12847 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
- avoid recomputing CAMLP4DEPS in the %.ml:%.ml4 rule
- a macro for compiling the tools by the best ocaml compiler
- use of $(if ...) rather that $ifdef
- some variables of Makefile.common were not that useful
(e.g. $(COQCCMX), which is $(COQCCCMO:.cmo=.cmx), used only once)
- the build of coqc.* should not depend upon coqtop, only its launch
(or I'm missing something)
- useless $(CAMLP4EXTENDFLAGS) variable
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12846 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12845 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
- support a new strategy: reduction using any of the allowed reduction
operators. This strategy does _not_ make the proof size grow.
- support rewriting under arbitrary [match with] using a folding
strategy. We fold matches to applications of registered [case]
combinators and let the user declare the Proper instances for them.
- fix the lemma application strategy to correctly report when no
progress has been made (avoids loop when repeateadly rewriting with
convertible terms).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12844 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12843 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
default solver (using "Set Firstorder Solver") and for program's
obligation tactic. I don't understand exactly the reason of the warning
when building states/initial.coq, anyone?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12842 85f007b7-540e-0410-9357-904b9bb8a0f7
|
herbelin
letouzey
vgross
notin
msozeau
barras
puech
thery