~jgross-h/coq/v8.2 : changes

~jgross-h/coq/v8.2 » Changes from revision 10138

From Revision 10117 to 10098

Rev	Summary	Authors	Date
10117	v8.2: Applying Xavier Leroy's patch for cmxs installation on... v8.2: Applying Xavier Leroy's patch for cmxs installation on cygwin (#3843).	Hugo Herbelin	9 years ago
10116	Fix guard condition for nested cofixpoints in checker. Fix guard condition for nested cofixpoints in checker. Conflicts: checker/inductive.ml	Maxime Dénès	10 years ago
10115	Fix guard condition for nested cofixpoints. Fix guard condition for nested cofixpoints. There were actually two problems, one of them being clearly unsound. To make sure that this does not show up somewhere else in the code, it would be better to resort to an abstraction keeping in sync the environment and the De Bruijn index of the current cofixpoints, like guard_env does for fixpoints. Conflicts: kernel/inductive.ml	Maxime Dénès	10 years ago
10114	Fix (3243): univ constraints of module subtyping were not pr... Fix (3243): univ constraints of module subtyping were not propagated Universe constraints coming from subtyping were not propagated to the outermost module and hence not stocked in the .vo file. Still, they were added to the interactive safe environment and hence checked for satisfiability.	Enrico Tassi	10 years ago
10113	Fix for critical bug in arity check. Fix for critical bug in arity check. Fix partially blind because Coq 8.2 does not compile with latest lablgtk.	Maxime Dénès	10 years ago
10112	configure stript allows make v4.00 configure stript allows make v4.00 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17042 85f007b7-540e-0410-9357-904b9bb8a0f7	pboutill	10 years ago
10111	v8.2: Fixing bug #3169 and avoiding anomaly in bug #2885 (vm... v8.2: Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute not supporting metas/evars). Fix of #3169 is by calling pretyping retyper rather than the non evar-aware kernel type-checker (since argument of vm_compute is supposed to be already typable).	Hugo Herbelin	10 years ago
10110	v8.2: Typo resulting in bad eta-expansion of destructing let... v8.2: Typo resulting in bad eta-expansion of destructing let's body.	Hugo Herbelin	10 years ago
10109	v8.2: Fixing a typo in the documentation of discriminate. v8.2: Fixing a typo in the documentation of discriminate. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@16554 85f007b7-540e-0410-9357-904b9bb8a0f7	herbelin	11 years ago
10108	Fixed #2839 and #2981 (anomaly NotASort in retyping). Was du... Fixed #2839 and #2981 (anomaly NotASort in retyping). Was due to collision between two variables of same name, but finally made a slightly different implementation of sort_of_atomic_type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@16188 85f007b7-540e-0410-9357-904b9bb8a0f7	herbelin	11 years ago
10107	v8.2: Fixed bug #2966 (de Bruijn error in computation of hea... v8.2: Fixed bug #2966 (de Bruijn error in computation of heads for coercions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@16171 85f007b7-540e-0410-9357-904b9bb8a0f7	herbelin	11 years ago
10106	v8.2: Fixed bug #2967 (missing check on ill-formed recursive... v8.2: Fixed bug #2967 (missing check on ill-formed recursive notation strings). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@16158 85f007b7-540e-0410-9357-904b9bb8a0f7	herbelin	11 years ago
10105	v8.2: Removed mention of configure's option -nowarning in IN... v8.2: Removed mention of configure's option -nowarning in INSTALL file. This option had actually never been released (it only existed for 2 days long in August 1999). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15904 85f007b7-540e-0410-9357-904b9bb8a0f7	herbelin	11 years ago
10104	v8.2: A few fixes in configure file: v8.2: A few fixes in configure file: - Fixing parsing of option -custom - More precise documentation of which option expects an argument - Deprecation of obviously obsolete -emacs option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15776 85f007b7-540e-0410-9357-904b9bb8a0f7	herbelin	11 years ago
10103	Bigint: adds a missing -1 in hugo's last commit 15659 Bigint: adds a missing -1 in hugo's last commit 15659 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15670 85f007b7-540e-0410-9357-904b9bb8a0f7	letouzey	11 years ago
10102	v8.2: Better fixing propagation of carry in sub_mult used fo... v8.2: Better fixing propagation of carry in sub_mult used for euclidian division over unbounded integers (thanks again to L. Théry for pointing out the remaining problem in r15640). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15662 85f007b7-540e-0410-9357-904b9bb8a0f7	herbelin	11 years ago
10101	Compatibility with camlp5 6.05 (Closes: #2728) Compatibility with camlp5 6.05 (Closes: #2728) Adapted from commit r15025. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15652 85f007b7-540e-0410-9357-904b9bb8a0f7	glondu	11 years ago
10100	Fix compilation with camlp5 in strict mode (Closes: #2487) Fix compilation with camlp5 in strict mode (Closes: #2487) Patch from Daniel de Rauglaudre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15651 85f007b7-540e-0410-9357-904b9bb8a0f7	glondu	11 years ago
10099	v8.2: Fixing unchecked overflow in sub_mult used for euclidi... v8.2: Fixing unchecked overflow in sub_mult used for euclidian division over unbounded integers (thanks to L. Théry for pointing out the problem). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15640 85f007b7-540e-0410-9357-904b9bb8a0f7	herbelin	11 years ago
10098	v8.2: Supporting optional byte-mark order in utf-8 files (bu... v8.2: Supporting optional byte-mark order in utf-8 files (bug #2757). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.2@15222 85f007b7-540e-0410-9357-904b9bb8a0f7	herbelin	12 years ago