coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cleaning CHANGES consistently with v8.4. Documenting COMPATIBILITY.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15711 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating version numbers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15709 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documenting eta-conversion.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15708 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More standard layout for \lambda in chapter CIC.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15707 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixup for macOS 10.8 & Ocaml 4.0	pboutill	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15704 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo in r15654	herbelin	2012-08-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15700 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating credits for final 8.4	herbelin	2012-08-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15699 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Avoid Pp.std_ppcmds in Misctypes.sort_info	letouzey	2012-08-07
\| \| \| \| \| \| \| \|	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
*	configure: two minor fixes for win32	letouzey	2012-08-07
\| \| \| \| \| \| \| \| \| \|	* 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
*	Vecnacentries.dump_global silently ignores exceptions	pboutill	2012-08-06
\| \| \| \| \| \|	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
*	Coqdoc inlined verbatim_char in latex	pboutill	2012-08-06
\| \| \| \| \| \|	Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15690 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add inline verbatim (<</>>), quotes (") and urls ({{url} name}) ↵	pboutill	2012-08-06
\| \| \| \| \| \|	markup/typesetting to coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15689 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Win32: some quote fixes	letouzey	2012-08-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15688 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MSetRBT: a tail-recursive plength	letouzey	2012-08-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15685 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Try to make the use of Unix.lockf in micromega compatible with Win32	letouzey	2012-08-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15684 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Dump references in Extraction	pboutill	2012-08-05
\| \| \| \| \| \|	Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15682 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Dump references in reduction tactics	pboutill	2012-08-05
\| \| \| \| \| \|	Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15681 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqdoc: More keywords, better special char escape, special case for "in *"	pboutill	2012-08-05
\| \| \| \| \| \|	Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15680 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Dump references	pboutill	2012-08-05
\| \| \| \| \| \|	Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15679 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More entries in the index	pboutill	2012-08-05
\| \| \| \| \| \|	Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15678 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Dump references in Reset	pboutill	2012-08-05
\| \| \| \| \| \|	Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15677 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revert "Fixing include printers"	pboutill	2012-08-05
\| \| \| \| \| \| \| \| \|	If you add Auto to dev/printers.mllib, then you have to add Tacmach, so you have to add Redexpr, consequently Vnorm is required, it depends on Vm, that include externals ! Let's revert commit 15675. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15676 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing include printers	ppedrot	2012-08-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15675 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Document the command Add/Remove Search Blacklist	letouzey	2012-08-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15674 85f007b7-540e-0410-9357-904b9bb8a0f7
*	re-sync CHANGES with 8.4	letouzey	2012-08-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15672 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bigint: new functions of_int and to_int, 2nd arg of pow in int	letouzey	2012-08-02
\| \| \| \| \| \| \| \| \| \| \| \|	* Many of_string and to_string could be replaced by of_int and to_int when the number isn't too large. NB: to_int may raise a Failure if the number is larger than max_int. * In numbers_syntax, computing the height of bigN trees via bigint is really overkill, int should be enough there : this limits printable/parsable bigN to (2^31)^(2^max_int) ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15669 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bigint: adds a missing -1 in hugo's last commit 15659	letouzey	2012-07-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15666 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bigint : better ensure canonicity of arrays of int blocks	letouzey	2012-07-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In the chosen representation of negative numbers, (-base) is actually legal as first element of an int array. This situation was wrongly handled by many functions in this module, leading to possible non-canonical representation of a big number, and hence faulty "equal" answers or buggy output of "to_string". For instance, on a 32-bit machine : open Big_int;; to_string (sub (of_string "-10000") (of_string "-1000000"));; (* was displaying 9810000 instead of 990000 *) Also simplified "of_string", which now rely on "neg" for handling negative numbers. Btw, improved checks comparing w.r.t OCaml's Big_int instead of float. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15665 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bigint: avoid dependency over Pp	letouzey	2012-07-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15664 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Better fixing propagation of carry in sub_mult used for euclidian	herbelin	2012-07-29
\| \| \| \| \| \| \|	division over unbounded integers (thanks again to L. Théry for pointing out the remaining problem in r15637). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15659 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing #2836 (materialize_evar might refine as a side effect the	herbelin	2012-07-29
\| \| \| \| \| \| \| \| \| \| \|	current evar to project; this may happen if this evar is dependent and is involved in evar-evar conversion problem eventually solved by instantiating the current evar; could maybe be optimized when the evar to materialize has invertible instance in which case define_evar_from_virtual_equation applied on the current evar could be shortcut, avoiding to create an evar). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15657 85f007b7-540e-0410-9357-904b9bb8a0f7
*	documentation of bullets (forward port from v8.4).	courtieu	2012-07-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15654 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix eta contraction in Reductionops	pboutill	2012-07-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15650 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug 2706: Coqide and layout that use special modifiers	pboutill	2012-07-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15649 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Same for Fin	pboutill	2012-07-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15648 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing bug #2835 (the rationale for printing notations was not	herbelin	2012-07-21
\| \| \| \| \| \|	standard under lambdas and products). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15644 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Improving management of notations with binders (see #2708 where a	herbelin	2012-07-21
\| \| \| \| \| \| \|	variable is used both as term and as binder, resulting in ununderstandable error message about scopes). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15642 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing unchecked overflow in sub_mult used for euclidian division over	herbelin	2012-07-21
\| \| \| \| \| \|	unbounded integers (thanks to L. Théry for pointing out the problem). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15637 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Slight modification to the printing of goals when in emacs mode.	courtieu	2012-07-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15635 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reductionops refactoring	pboutill	2012-07-20
\| \| \| \| \| \| \| \| \| \| \|	Semantic changes are : - whd_nored_stack remplaces a defined meta by its value whereas the old whd_stack didn't. - Zcase and Zfix are alwais put on stack. iota_flag is checked by constructors and cofix. - simpl uses its own whd_ function that do not touch at matched term git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15634 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixup implicits in patterns & notations	pboutill	2012-07-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15633 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Vector equalities first stuff	pboutill	2012-07-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15632 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Put Option in Clib	pboutill	2012-07-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15631 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing test-suite	pboutill	2012-07-20
\| \| \| \| \| \| \| \|	- bug in r15614: hnf was identity - fix Print Assumptions - bug in r15624: Dump glob of Print About only for Glob git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15630 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Let coqtop be a little more stupid in hint answer: otherwise, that	ppedrot	2012-07-20
\| \| \| \| \| \| \|	may blow up computation time by carelessly reducing potentially huge terms. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15628 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Getting rid of the undocumented [complete] tactic, which was	ppedrot	2012-07-19
\| \| \| \| \| \| \|	redundant with [solve]. The AST node still exists in Ltac, because this is used by the [assert ... by ...] tactical. Fixes #2847. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15625 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Various minor fixes to coqdoc from A. Chlipala.	msozeau	2012-07-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15624 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added abstration layer to goal display in CoqIDE, and cleaned parts	ppedrot	2012-07-16
\| \| \| \| \| \|	of the code altogether. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15623 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing goal display when still focussing but no more goals.	ppedrot	2012-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15622 85f007b7-540e-0410-9357-904b9bb8a0f7