aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2009-01-18Getting rid of the previous implementation of setoid_rewrite which wasmsozeau
unplugged a long time ago. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11798 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-18Last changes in type class syntax: msozeau
- curly braces mandatory for record class instances - no mention of the unique method for definitional class instances Turning a record or definition into a class is mostly a matter of changing the keywords to 'Class' and 'Instance' now. Documentation reflects these changes, and was checked once more along with setoid_rewrite's and Program's. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11797 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-17DISCLAIMERpuech
========== This big patch is commited here with a HUGE experimental tag on it. It is probably not a finished job. The aim of committing it now, as agreed with Hugo, is to get some feedback from potential users to identify more clearly the directions the implementation could take. So please feel free to mail me any remarks, bug reports or advices at <puech@cs.unibo.it>. Here are the changes induced by it : For the user ============ * Search tools have been reimplemented to be faster and more general. Affected are [SearchPattern], [SearchRewrite] and [Search] (not [SearchAbout] yet). Changes are: - All of them accept general constructions, and previous syntactical limitations are abolished. In particular, one can for example [SearchPattern (nat -> Prop)], which will find [isSucc], but also [le], [gt] etc. - Patterns are typed. This means that you cannot search mistyped expressions anymore. I'm not sure if it's a good or a bad thing though (especially regarding coercions)... * New tool to automatically infer (some) Record/Typeclasses instances. Usage : [Record/Class *Infer* X := ...] flags a record/class as subject to instance search. There is also an option to activate/deactivate the search [Set/Unset Autoinstance]. It works by finding combinations of definitions (actually all kinds of objects) which forms a record instance, possibly parameterized. It is activated at two moments: - A complete search is done when defining a new record, to find all possible instances that could have been formed with past definitions. Example: Require Import List. Record Infer Monoid A (op:A->A->A) e := { assoc : forall x y z, op x (op y z) = op (op x y) z; idl : forall x, x = op x e ; idr : forall x, x = op e x }. new instance Monoid_autoinstance_1 : (Monoid nat plus 0) [...] - At each new declaration (Definition, Axiom, Inductive), a search is made to find instances involving the new object. Example: Parameter app_nil_beg : forall A (l:list A), l = nil ++ l. new instance Build_Monoid_autoinstance_12 : (forall H : Type, Monoid (list H) app nil) := (fun H : Type => Build_Monoid (list H) app nil ass_app (app_nil_beg H) (app_nil_end H)) For the developper ================== * New yet-to-be-named datastructure in [lib/dnet.ml]. Should do efficient one-to-many or many-to-one non-linear first-order filtering, faster than traditional methods like discrimination nets (so yes, the name of the file should probably be changed). * Comes with its application to Coq's terms [pretyping/term_dnet.ml]. Terms are represented so that you can search for patterns under products as fast as you would do not under products, and facilities are provided to express other kind of searches (head of application, under equality, whatever you need that can be expressed as a pattern) * A global repository of all objects defined and imported is maintained [toplevel/libtypes.ml], with all search facilities described before. * A certain kind of proof search in [toplevel/autoinstance.ml]. For the moment it is specialized on finding instances, but it should be generalizable and reusable (more on this in a few months :-). The bad news ============ * Compile time should increase by 0 to 15% (depending on the size of the Requires done). This could be optimized greatly by not performing substitutions on modules which are not functors I think. There may also be some inefficiency sources left in my code though... * Vo's also gain a little bit of weight (20%). That's inevitable if I wanted to store the big datastructure of objects, but could also be optimized some more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11794 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-16Correct a bug in commit 11659puech
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11792 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-15Patch by Brian Campbell to output more information on the exception thatmsozeau
made a glob file unreadable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11788 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-14Fixing #1960 (xml bug with external on goal variable) and #1961herbelin
(anomaly while parsing $ not followed by an ident). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11785 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-14Fixing/improving management of uniform prefix Local and Globalherbelin
modifiers (added a "Syntax Checking" phase for raising a non interpretation error just after a dot is parsed -- maybe exaggerated complication for what we want to do ?). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11783 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-13Updated datesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11782 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-13- Standardized prefix use of "Local"/"Global" modifiers as decided inherbelin
late 2008 Coq WG. - Updated Copyright file wrt JProver. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11781 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-13Workaround to compile the coq archive with dynamic loading on Mac OS 10.5herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11777 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-12Fix a bunch of bugs related to setoid_rewrite, unification and evars:msozeau
- Really unify with types of metas when they contain metas _or_ evars (why not always?) (fixes bug #2027). - Better handling of evars in rewrite lemmas when using setoid_rewrite through rewrite (reported by Ralf Hinze). - Use retyping with metas when possible (check?) and improve an obscure error message in retyping. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11776 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-11- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).herbelin
- Added dependency of mltop.ml4 into config/Makefile (see bug #2023). - Fixed bug #1963 (dependent inversion building a universe-ill-formed conversion problem). - Incidentally, moved "Large non-propositional inductive ..." error message to standard himsg.ml error displayer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11774 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-10Another problem with blanks in filenamesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11773 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-10- Fixed the recompilation of config/revision.ml once every two conmpilations.herbelin
- Fixed an error message in configure - Support for filenames with spaces in coqmktop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11772 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-09Oups... il n'y a pas d'option -impl pour ocamldepnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11771 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 21:48:59 +0000