aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2009-02-09commited complexity test for exponential behavior of unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11894 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-09memoized is_ground_envbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11893 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-06pushed evar reduction in kernelbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-06Fixed bug #2036 (wrong copy-paste in RIneq) [copy of 11887 in branch v8.2]herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11888 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-06Fixing #2044 (bad printing of primitive notation at the head ofherbelin
coercion to funclass) [added a new notation output test as the initial one is quite saturated in miscellaneous notations]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11886 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-06From v8.2 to trunk:herbelin
- commit 11871 (Miller's pattern detection bug) + a corresponding test - commit 11883 (.ml4 to .cmxs in coq_makefile) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11884 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-04Fix [subrelation] clauses that privileged the weakest. Better impl argsmsozeau
for [PartialOrder] typeclass. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11882 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-04Report r11631 from 8.2 and handle non-dependent goals better inmsozeau
[dependent induction]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11881 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-04Fix d'un bug avec l'option gallinanotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11880 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-03Do not reserve the keyword "Infer".puech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11879 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-03Allow to turn contrib/subtac into a (nat)dynlink'able pluginletouzey
Main issue was declare_summary being triggered too late in subtac_obligations, hence the associated init_function was _not_ being done by Lib.init(). Fixed for the moment by an ad-hoc launch of this init_function in subtac_obligations. In other plugins, this issue doesn't appear, since init_function is mostly putting back some empty set into a reference that was initially empty. No need to really run init_function in this case. For future plugins, we will nonetheless have to be careful about that. Of course, the (ref Obj.magic) was not exactly helpful in debugging this matter, see http://caml.inria.fr/mantis/view.php?id=4707 As said by Xavier, naughty naughty boys... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11877 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-03Fix the installation of plugins (both initial and late ones)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11876 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-31Reorder coqmktop options and document -echoglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11875 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-30More portable way to pipe stderrglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11874 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-30Correction bug 2037.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11873 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-29Solves some warning and hides some not-bad ones in doc. It remains aherbelin
few hevea warning (failure to put a vector on an expression in Classes.tex, failure to support multirow in RecTutorial.tex). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11868 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-28FSet(Weak)List : eq_dec becomes Defined (and gets better proof)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11867 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-27- Fixed various Overfull in documentation.herbelin
- Removed useless coq-tex preprocessing of RecTutorial. - Make "Set Printing Width" applies to "Show Script" too. - Completed documentation (specially of ltac) according to CHANGES file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11863 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-27Cleaned CHANGES (rough backport of 11855 from v8.2 to trunk).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11862 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-27Forgot a file in r11859. Sorry...puech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11860 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-26Revert changes in pcoq functions to restore compatibility with contribspuech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11859 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-23Suppression de l'ancien logo (problèmes de droits)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11854 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-23Really compare evar maps in progress, due to merging in apply and othermsozeau
tactics, an unchanged map may have a different adress. Part of the fix for making Ynot work in 8.2. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11852 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-23Petit nettoyage faisant suite au commit #11847 .aspiwack
Quelques modifications autour (géographiquement) de Util.list_split_at Util.list_split_at devient Util.list_split_when (dénomination inventée arbitrairement par moi-même, mais qui ne devrait pas déranger grand monde vu qu'il semble n'y avoir que deux occurences de cette fonction). Pour laisser la place à la fonction suivante : Introduction de Util.list_split_at: qui sépare la liste à une position donnée (alors que la nouvellement nommé list_split_when sépare à la première occurence "vrai" d'un prédicat). Ajout de quelques commentaires dans util.ml (pas le mli) sur ces deux fonctions. Suppression de Impargs.list_split_at (appel à Util). Suppression de Subtac_pretyping.list_split_at (qui était du code mort de toute façon). Suppression Util.list_split_by qui n'est utilisé nulle part et est une réimplémentation de List.partition (qui est probablement meilleure, en particulier tail-recursive) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11851 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-22Fix #2011 : an incorrect environment when extracting Module ... with ...letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11848 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-22Util.split_at : for quadratic to linear complexityletouzey
This function is probably used only on small lists, but it's not a reason to let it be quadratic... I'm wondering how many other inefficient functions like this one may exist in the source of Coq. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11847 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-22Extraction Library works now when some files share the same short name (fix ↵letouzey
#2025) For instance, when we need to extract Init.Wf and Program.Wf, the first one gives wf.ml and the second wf0.ml. This name resolution mechanism is merged with the handling of the extraction filename blacklist. Hence, after Extraction Blacklist Foo, the coq file Foo.v will now be extracted as foo0.ml (instead of coq_Foo.ml as previously). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11843 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-22Fixes in the documentation of [dependent induction] and test-suitemsozeau
scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11839 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-22configure: more adequate message explaining what -opt is doingletouzey
No, -opt has nothing to do with compilation to native or byte-code, nor has it anything to do with the "generation of optimized executables". It simply mean to try to use ocamlc.opt and ocamlopt.opt if they exist. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11837 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-22Fix d'un petit problème avec ocamlmklib en présence de l'option -camldirnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11834 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-22Remplacement de cp --parents par un script shnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11833 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-21Fixed bug 2030 (bad syntax for "test" in doc compilation) [see 11824herbelin
from v8.2 branch]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11825 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-21Fix bug #2004 due to bad handling of evars in the unification for msozeau
the setoid_rewrite variant called by rewrite (bug traced by Hugo). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11822 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-21- Better deal with commands inside section titles in latex output usingmsozeau
the support from hyperref. - Rename n-ary 'exist' tactic to 'exists' in Program.Syntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11821 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20Fixing bug #1918 (no occur-check in Meta unification was done yet!).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11818 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20- Fixing bug 1891 (abusive instantiations of evar arguments inherbelin
evar-evar problems). - Fixing target "make programs". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11817 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20Fixing a bug in 11804 (support for _ in ident entry of notations). herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11816 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20Added some missing statements for proof folding and correctedvgross
the reference manual accordingly git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11815 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20Added proof folding into CoqIde. See RefMan for using it.vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11814 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20Cette version là fonctionne correctement au moins pour certaines aspiwack
architectures. Désolé pour les cafouillages. Si quelqu'un a des ennuis en installant un trunk prévenez moi, c'est sûrement ma faute. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11813 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20More fixes... aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11812 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20Un fix sur le commit précédent. aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11811 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20Patch de l'installation:aspiwack
Quand les plugins sont activés, ils devraient être installés par make install. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11810 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-19Les records déclarés avec Record ne peuvent plus être récursifs (le aspiwack
comportement est similaire à la 8.1). Les records récursifs peuvent-être déclarés avec Inductive et CoInductive, avec les effets idoines sur leur nature. J'ai fait quelques changements dans VernacInductive pour que tout ceci fonctionne bien ensemble. Il reste du nettoyage à faire et probablement des ajustement dans le Printing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11808 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-19Propriétés svn pour les filtres latexnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11807 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-19Experimental file commited by mistake, sorry.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11806 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-19The initial state evar numbering increased. Fix output message in a test.puech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11805 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-19- Structuring Numbers and fixing Setoid in stdlib's doc.herbelin
- Adding ability to use "_" in syntax for binders (as in "exists _:nat, True"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11804 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-18Backporting from v8.2 to trunk:herbelin
- Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-18Various little fixes:msozeau
- allow a new line after a (** printing *) directive in coqdoc so as not to output spurious new lines. - never directly unify the lemma with an evar in setoid_rewrite (they act as opaque constants). - Fix a useless dependency introduced by tauto which splits a record in SetoidList. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11799 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-21 18:08:00 +0000