aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2009-01-08Remove trailing newlines in outputs of X -whereglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11768 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-08Minor doc fixes:msozeau
- Set BIBINPUTS variable correctly so that we do not use any random biblio.bib file. - Update setoid_rewrite doc to new typeclasses syntax and fix verb -> texttt - Stop using less than 100% line heights in coqdoc.css git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11767 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-07Uniformisation of some error messages + added test on setoid rewrite.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11765 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-07Fixing a cosmetic tactic printer bug in passingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11764 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-07Sous Windows, 'coqtop -where' renvoit des chemins contenant des '\'notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11761 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-07Fix build for git usersglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11760 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-07Suite de la révision #11756notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11757 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-06Conversion du fichier 'revision' en un fichier .ml + correction d'un bug ↵notin
dans le configure introduit par les révisions 11754 et 11755 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11756 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-06Report de la révision 11754 (compilation sous windows)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11755 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-06Installation des librairies: on utilise maintenant LINKCMO au lieu denotin
l'appel à find. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11753 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-05Completed 11745 (move of jprover to user contribs) and cleaned 11743herbelin
(detection of Miller's pattern) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11748 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-04Added installation of .cmi files in "make install" target of coq_makefile.herbelin
Updated CHANGES. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11747 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-04Moved JProver to a user contribution (as was decided a long time ago)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11746 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-04Bug dans commit 11743herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11744 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-04Fixed bugs #2001 (search_guard was overwriting the guard index givenherbelin
by user) and #2017 (unification pattern test too crude leading to regression wrt to 8.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11743 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-03Fixed two problems:herbelin
- Function descend_in_conjunctions was now too weak, use match_with_record. - Added documentation of new notation for destruct with equation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11742 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-02Regression test for bug #1967herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11740 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-02Conséquence renommage canonique de refl_equal en eq_refl.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11736 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-02Made the debugger work again:herbelin
- call to open_process_full from Envars.camlp4lib was apparently disturbing stdin/stdout/stderr and precipitating coqtop.byte death in ocamldebug; renounced to add camlp4 to the ml path (why was it useful?) which was the reason for calling camlp4lib (seems like camlp4lib is now useless), - Envars was needing str.cma which was missing when calling printers.cma; renounced to use str.cma since its only use was for an elementary split function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11734 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-02Fixed two apparent inconsistencies in matching.ml:herbelin
- matching_subterm was activating partial_app to true in matches_core even when no partial_app was expected, - "match goal" (hence "extended_matches") was called with partial_app in 8.2 (currently "matches" but not in trunk; what to do with (legacy) "matches" remains unclear. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11733 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-02- Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",herbelin
and, with a now generic intropattern "[]", also "as []_eqn", "as []_eqn:H" for "destruct" with equality keeping. - Fixed an accuracy loss in error location. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11732 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-01Updateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11730 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-01Switched to "standardized" names for the properties of eq andherbelin
identity. Add notations for compatibility and support for understanding these notations in the ml files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11729 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-01- Fixed bug #2021 (uncaught exception with injection/discriminate whenherbelin
the inductive status of a projectable position comes from a dependency). - Improved doc of the stdlib chapter (see bug #2018), and fixed tex bugs introduced in r11725. - Applied wish #2012 (max_dec transparent). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11728 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added shortcuts for "fst (decompose_prod t)" and co. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11727 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-30- Fixed bugs and compatibilities issues in herbelin
match_conjunction/match_disjunction/array_for_all_i - Finally activate fine-tuned unfolding of iff in tauto: it breaks at only one place in the user contribs (FSetAVL_dep.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11726 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-15 06:37:53 +0000