aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-08-24Experimental support for a comment in the files' preamble in extraction.aspiwack
Scheme comments are output on a single line because Ocaml's Format module which serves as a backend to Pp has an integer, rather than a string as identation value, so we cannot make it so that each new line in the comment starts with ";; ". I've tried something with Pp.ifb but it was hackish at best and had somewhat strange results. Known bug: as Pp.std_ppcmds is non-persistent, the comment is actually printed only once per Extraction command, even if it outputs several files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15763 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24Add option Set/Unset Extraction Conservative Types.aspiwack
Extracted code need not preserve typing relations (e:t) from the source code. This may be a problem as the extracted code may not implement the intented interface. This option disables the optimisations which would prevent an extracted term's type to be its extracted source term's type. At this point the only such optimization is (I think) removing some dummy λ-abstractions in constant definitions. Extraction Implicit is still honored in this mode, and it's mostly necessary to produce reasonable types. So in the conservative type mode, which abstractions can be removed and which can'tt is entirely under the user's control. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15762 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24Better highlighting of strings in coqide.aspiwack
Strings were not highlighted out of comments. This would lead to funny result, like certain strings (i.e. "(*") to cause all following code to be highlighted as a string. I've added strings in three different contexts (the same where comments are highlighted). I think it's safe to do, I don't know if it's the best way, though. In particular I don't know if it's the best way to highlight notations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15761 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24Assumption commands are now displayed as unsafe in Coqide.aspiwack
They are still marked as safe if they are part of a module type, though. Also local assumptions such as "Hypothesis" or "Context" are displayed as unsafe if they happen to be defined without a section. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15760 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24Modification of the unjustified tag.aspiwack
It seemed to intrusive to have it display the text underlined and red. The goal of this tag is to notify the user when Coq doesn't guarantee correctness, not to make the command look like an error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15759 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24Correcting a comment in pattern-matching compilation.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15758 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23test-suite: Local Tactic Notation is now legal since r15731letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15757 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23CHANGES: document the end of states/initial.coq and coqtop.optletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15756 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23Remove a script unused since 2006 (cf commit r8626)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15755 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23myocamlbuild : fixes for new printing directory + sourceview for coqideletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15754 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23No more states/initial.coq, instead coqtop now requires Prelude.voletouzey
For starting a bare coqtop, the recommended option is now "-noinit" that skips the load of Prelude.vo. Option "-nois" is kept for compatibility, it is now an alias to "-noinit". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23No more coqtop.opt, produce directly a coqtop binaryletouzey
We now always produce two binaries, coqtop and coqtop.byte : - If ocamlopt is available, coqtop is directly what used to be coqtop.opt, no more symlinks needed. - Otherwise, coqtop is a copy of coqtop.byte. The same for coqchk and coqide... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15752 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23No need anymore to refer to COQLIB in ocamldebug-coqletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15751 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23Revert "when cross-compiling with mingw32, let's fix the Filename.dir_sep"letouzey
This was merely cosmetic after all, since recent Windows versions do tolerate paths with /. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15750 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23Configure + Makefile : simplification when -localletouzey
When local=true: - "make install" is now a no-op - In configure, no need hence to fill the various variables about installation (BINDIR, COQLIBINSTALL, MANDIR, DOCDIR, EMACSLIB). This avoids many references to absolute location of the coq sources (which may contain blanks or other strange chars in win32). - For the moment, we keep CONFIGDIR and DATADIR, used when launching coqide from inside the build directory. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15749 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23configure: get rid of the -src option and of ${COQSRC}letouzey
The -src option was antic and probably broken (many references to source files without the $COQRSC prefix). Instead, it's quite simpler to refer to paths in relative way (and safer in win32 where the base path may include spaces and other horrors). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15748 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23configure: no more need for ocamlmktopletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15747 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23Extraction: document Separate Extraction and KeepSingletonletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15746 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23Simpler configure: gcc via ocamlc, no ranlib (done by ocamlmklib)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15745 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23Port from 8.4 branch some build fixes concerning win32 :letouzey
r15722: - CAMLBIN was cygwin-specific, leading to issues with coqmktop - A missing Filename.quote on the temp file used in coqmktop - Try to shorten the cmdline passed to Sys.command in coqmktop: way too many includes were passed to coqmktop -boot r15724: Coqmktop: the +compiler-libs for ocaml4 is back r15725: Coqmktop: better detection of ocaml 4 and above r15739: ocamlbuild : a missing include for camlp4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15744 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-22Do not forget to build the unicode libraries, necessary to compile and ↵msozeau
launch coqtop in utf mode. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15743 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-11Improving rendering of ldots in doc (partially done, there are tooherbelin
much of them). Improving doc of conversion clauses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15733 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-11Some extra INCOMPATIBILITIES since 8.4.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15732 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15731 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-11Some changes in CHANGES.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15730 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-11Improving rendering of ...-separated lists and sequences in referenceherbelin
manual (making style uniform: no {\tt \ldots}; using only one space when there is no delimiters in the sequence). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15729 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-11fast bitwise operations (lor,land,lxor) on int31 and BigNletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-10Bug 2861 : ocamlopt but no lablgtk2.cmxa problempboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15721 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-10Fixes bug #2857.aspiwack
Coqide used the wrong escape sequence to delimit coq phrases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15720 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-09Unification in Evar_conv uses an abstract machine statepboutill
It uses a term in front of a stack instead of a term in front of a list of applied terms. From outside of eq_appr_x nothing should have changed. Nasty evar instantiation bug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15719 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Cleaning CHANGES consistently with v8.4. Documenting COMPATIBILITY.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15711 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating version numbers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15709 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Documenting eta-conversion.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15708 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08More standard layout for \lambda in chapter CIC.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15707 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Fixup for macOS 10.8 & Ocaml 4.0pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15704 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-07Typo in r15654herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15700 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-07Updating credits for final 8.4herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15699 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-07Avoid Pp.std_ppcmds in Misctypes.sort_infoletouzey
Otherwise, after a Set Printing Universes we may end on a comparison of Pp.std_ppcmds, which may fail on functional values (cf. Constrextern.check_same_type), as notice by Pierre-Marie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15697 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-07configure: two minor fixes for win32letouzey
* ocamlc -version may end with a \r in win32 (fix #2849) * $COQSRC may initially be cygwin-specific and hence rejected by ocaml. For the moment, an ad-hoc fix is to remove the problematic $COQSRC, and mark the -src option as incompatible with win32... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15696 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-06Vecnacentries.dump_global silently ignores exceptionspboutill
So PrintName and Extraction dump globals when they exist git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15691 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-06Coqdoc inlined verbatim_char in latexpboutill
Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15690 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-06Add inline verbatim (<</>>), quotes (") and urls ({{url} name}) ↵pboutill
markup/typesetting to coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15689 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-06Win32: some quote fixesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15688 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-06MSetRBT: a tail-recursive plengthletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15685 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-06Try to make the use of Unix.lockf in micromega compatible with Win32letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15684 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-05Dump references in Extractionpboutill
Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15682 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-05Dump references in reduction tacticspboutill
Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15681 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-05Coqdoc: More keywords, better special char escape, special case for "in *"pboutill
Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15680 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-05Dump referencespboutill
Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15679 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:04:55 +0000