aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Solves some warning and hides some not-bad ones in doc. It remains aGravatar herbelin2009-01-29
| | | | | | | | | 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
* FSet(Weak)List : eq_dec becomes Defined (and gets better proof)Gravatar letouzey2009-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11867 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed various Overfull in documentation.Gravatar herbelin2009-01-27
| | | | | | | | | | - 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
* Cleaned CHANGES (rough backport of 11855 from v8.2 to trunk).Gravatar herbelin2009-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11862 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgot a file in r11859. Sorry...Gravatar puech2009-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11860 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert changes in pcoq functions to restore compatibility with contribsGravatar puech2009-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11859 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'ancien logo (problèmes de droits)Gravatar notin2009-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11854 85f007b7-540e-0410-9357-904b9bb8a0f7
* Really compare evar maps in progress, due to merging in apply and otherGravatar msozeau2009-01-23
| | | | | | | | 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
* Petit nettoyage faisant suite au commit #11847 .Gravatar aspiwack2009-01-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Fix #2011 : an incorrect environment when extracting Module ... with ...Gravatar letouzey2009-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11848 85f007b7-540e-0410-9357-904b9bb8a0f7
* Util.split_at : for quadratic to linear complexityGravatar letouzey2009-01-22
| | | | | | | | 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
* Extraction Library works now when some files share the same short name (fix ↵Gravatar letouzey2009-01-22
| | | | | | | | | | | | | | #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
* Fixes in the documentation of [dependent induction] and test-suiteGravatar msozeau2009-01-22
| | | | | | | scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11839 85f007b7-540e-0410-9357-904b9bb8a0f7
* configure: more adequate message explaining what -opt is doingGravatar letouzey2009-01-22
| | | | | | | | 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
* Fix d'un petit problème avec ocamlmklib en présence de l'option -camldirGravatar notin2009-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11834 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de cp --parents par un script shGravatar notin2009-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11833 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug 2030 (bad syntax for "test" in doc compilation) [see 11824Gravatar herbelin2009-01-21
| | | | | | | | from v8.2 branch]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11825 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2004 due to bad handling of evars in the unification for Gravatar msozeau2009-01-21
| | | | | | | 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
* - Better deal with commands inside section titles in latex output usingGravatar msozeau2009-01-21
| | | | | | | | 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
* Fixing bug #1918 (no occur-check in Meta unification was done yet!).Gravatar herbelin2009-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11818 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixing bug 1891 (abusive instantiations of evar arguments inGravatar herbelin2009-01-20
| | | | | | | | | 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
* Fixing a bug in 11804 (support for _ in ident entry of notations). Gravatar herbelin2009-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11816 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added some missing statements for proof folding and correctedGravatar vgross2009-01-20
| | | | | | | | the reference manual accordingly git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11815 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added proof folding into CoqIde. See RefMan for using it.Gravatar vgross2009-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11814 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cette version là fonctionne correctement au moins pour certaines Gravatar aspiwack2009-01-20
| | | | | | | | | | 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
* More fixes... Gravatar aspiwack2009-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11812 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un fix sur le commit précédent. Gravatar aspiwack2009-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11811 85f007b7-540e-0410-9357-904b9bb8a0f7
* Patch de l'installation:Gravatar aspiwack2009-01-20
| | | | | | | | | 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
* Les records déclarés avec Record ne peuvent plus être récursifs (le Gravatar aspiwack2009-01-19
| | | | | | | | | | | | | | 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
* Propriétés svn pour les filtres latexGravatar notin2009-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11807 85f007b7-540e-0410-9357-904b9bb8a0f7
* Experimental file commited by mistake, sorry.Gravatar herbelin2009-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11806 85f007b7-540e-0410-9357-904b9bb8a0f7
* The initial state evar numbering increased. Fix output message in a test.Gravatar puech2009-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11805 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
| | | | | | | | - 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
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
| | | | | | | | | | - 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
* Various little fixes:Gravatar msozeau2009-01-18
| | | | | | | | | | | | - 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
* Getting rid of the previous implementation of setoid_rewrite which wasGravatar msozeau2009-01-18
| | | | | | | unplugged a long time ago. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11798 85f007b7-540e-0410-9357-904b9bb8a0f7
* Last changes in type class syntax: Gravatar msozeau2009-01-18
| | | | | | | | | | | | - 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
* DISCLAIMERGravatar puech2009-01-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ========== 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
* Correct a bug in commit 11659Gravatar puech2009-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11792 85f007b7-540e-0410-9357-904b9bb8a0f7
* Patch by Brian Campbell to output more information on the exception thatGravatar msozeau2009-01-15
| | | | | | | made a glob file unreadable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11788 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing #1960 (xml bug with external on goal variable) and #1961Gravatar herbelin2009-01-14
| | | | | | | | (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
* Fixing/improving management of uniform prefix Local and GlobalGravatar herbelin2009-01-14
| | | | | | | | | | 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
* Updated datesGravatar herbelin2009-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11782 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Standardized prefix use of "Local"/"Global" modifiers as decided inGravatar herbelin2009-01-13
| | | | | | | | | 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
* Workaround to compile the coq archive with dynamic loading on Mac OS 10.5Gravatar herbelin2009-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11777 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a bunch of bugs related to setoid_rewrite, unification and evars:Gravatar msozeau2009-01-12
| | | | | | | | | | | | - 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
* - Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).Gravatar herbelin2009-01-11
| | | | | | | | | | | | - 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
* Another problem with blanks in filenamesGravatar herbelin2009-01-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11773 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed the recompilation of config/revision.ml once every two conmpilations.Gravatar herbelin2009-01-10
| | | | | | | | - 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
* Oups... il n'y a pas d'option -impl pour ocamldepGravatar notin2009-01-09
| | | | 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.39.1) at 2024-09-08 07:48:11 +0000