aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2008-12-02fixed kernel bug (de Bruijn) + test-suitebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11646 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-28another bug with simplbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11644 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-28Inductive parameters: nicer doc examples and error messageletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11642 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-27Test case for previous commit.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11641 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-27Fix (?) a pattern matching compilation problem: msozeau
<< Axiom A : nat -> bool. Definition foo := match A 0 with | true => true | k => k end. Print foo. >> [A 0] is duplicated in the [k => k] branch! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11640 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-27fixed non-exhaustive pattern matchingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11638 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-27fixed bug 1791: simpl was performing eta expansionbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11636 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-27added tests for hyps reorderingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11635 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-27fixing problem with CompCert: reordering resulting from tac change was not ↵barras
closed w.r.t. dependencies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11634 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-26closed bug 1898: fold x in x; added a reordering primitive tacticbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11633 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-26closed bug 1898: fold x in x; added a reordering primitive tacticbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11632 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-25correction bug 1997.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11630 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-24eventually fixing r11612barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11626 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-24amelioration mineur du comportement de Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11625 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-23first attempt to allow Function to deal with dependent pattern matching. ↵jforest
This Functionnality is VERY VERY experimental and only works with non recursive functions and structurally defined function git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11624 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-23- Synchronized subst_object with load_object (load_and_subst_objects)herbelin
and set Declare ML Module as a regular substitutive object so that Declare ML Module is treated at the right place in the order of appearance of substitutive declarations of a required module. - Note: The full load/import mechanism for modules is not so clear: the Require part of a Require Import inside a module is set outside the module at module closing but the Import part remains inside (why not to put the "special" objects in the module too?); moreover the "substitute" and "keep" objects of a module are desynchronised at module closing (is that really harmless/necessary?). - Treatment of .cmxs targets in coq_makefile and in coqdep. - Better make clean in coq_makefile generated makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11623 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-23Fine-tuning rewriting from "eq_true b": using <- to rewrite true to bherbelin
(if ever necessary). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11621 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-23Minor improvement to commit 11619herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11620 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-23Fixed bug #2006 (type constraint on Record was not taken into account) +herbelin
slight improving of the printing of record. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11619 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-22Fixed bug in VernacExtend printing + missing vernacular printing rules +herbelin
revival of option -translate as a -beautify option. PS: compilation checked against 11610. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11618 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-22- Fixed minor bug #1994 in the tactic chapter of the manual [doc]herbelin
- Improved warning when found several path to the same file in path [mltop.ml4, system.ml] - Add support for "rewrite" on specific equality to true (i.e. eq_true) [Datatypes.v, tactics] PS: compilation test made over 11611 to shunt the archive-breaking 11612 and 11614 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11617 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-21fixed problem with r11612barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11614 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-21fixed exponential behavior of evar unif (ground case)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11612 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-20correction of bug #2002jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11610 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-19Add implicit rules for native plugins (.cmxs)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11607 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-19Execute #rectypes directive in embedded OCaml toplevel...glondu
...to avoid the need to have cflags.cmi around. This directive will likely be available in the next version of OCaml. See OCaml bug #4460. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11605 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-19Fix typo in omega docglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11604 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-17integrate suggestions by B. Baydemir (see #1930)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11600 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-16Univ: two < instead of a Pervasives.compare on int (as suggested by X. Leroy)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11595 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-15Correct display of constraints for Print Universes "dumpfile"letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11593 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-14Amélioration du README.doc et de l'installation de la docnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11591 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-14Restores behaviour of v8.1 for unification problems which fail (backport of ↵letouzey
11585) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11590 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-14Faster comparison of universesletouzey
- compare the integer indexes first, in order to avoid comparing the dirpath part if possible - use an ad-hoc comparison function rather than Pervasives.compare (slightly faster during my tests on the compcert contrib) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11589 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-14make doc ne compilait plus la doc de stdlib (bug #1996)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11588 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-14Add missing test-suite files for closed bugs.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11587 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-14retour sur le commit 11579 qui faisait plante les contribs FSet et color.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11586 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-13Tentative d'amélioration de la robustesse des Makefile générés parnotin
coq_makefile en présence de fichiers .ml : - ajout d'une option -config à coqtop qui affiche les informations de configuration (COQTOP, COQBIN, COQLIB, CAMLP4, CAMLP4LIB, CAMLBIN, LOCAL) - coq_makefile inclut un fichier Makefile.config qui contient les valeurs des variables sus-mentionnées git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11584 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-13git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11583 ↵barras
85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-12Correction du bug #1995notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11580 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-12Les signatures des applications de foncteur sont précalculées, cela ↵soubiran
alourdit un peu les vo mais accélère la compilation lorsque les foncteurs sont massivement utilisés. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11579 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-10Makefile.build: an OPTFLAGS behind a bytecode ocamlc (which refuses -p)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11577 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-10Fix mixup between Record, Structure and Class by adding a new variant formsozeau
the three cases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11572 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-10Fix bug reported by Mark Dickinson on Coq-Club about [setoid_rewrite] notmsozeau
reducing the type of the given lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11571 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09- Correction erreur dans test output Notation.vherbelin
- Ajout test pour non-régression du bug #1968 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11569 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09f_equal : solve an inefficiency issue (apply vs. simple apply)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11567 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09better fix for #1931 by using sort_ofletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11566 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09Oops... forgot to commit a file related to r11561.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11565 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09Add test-suite file related to discussion of syntax of implicit binders.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11564 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09More factorization of inductive/record and typeclasses: move classmsozeau
declaration code to toplevel/record, including support for singleton classes as definitions. Parsing code also factorized. Arnaud: one more thing to think about when refactoring the definitions in vernacentries. Add support for specifying what to do with anonymous variables in contexts during internalisation (fixes bug #1982), current choice is to generate a name for typeclass bindings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11563 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-09- Fixed bug 1968 (inversion failing due to a Not_found bug introduced inherbelin
Evarutil.check_and_clear_in_constr in V8.2 revision 11309 and trunk revision 11300). - Improved various error messages related to inversion, evars and case analysis (including the removal of the obsolete dependent/non dependent distinction). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11561 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-07 20:54:02 +0000