aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2009-08-19adds a property on mapbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12285 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-19adds lemmas on interactions between existsb, forallb, and appbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12284 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-15+ csdp.cachefbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12283 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-14Mise à jour du document de révision de la stdlib et déplacement de laherbelin
proposition de nommage standardisé des lemmes dans le trunk. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12282 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-14+Fix interface.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12281 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-14Ajout de la gestion de Local et Global pour les options (au sens deaspiwack
Goptions). - Local Set/Unset ... change la valeur de l'option pour la section en cours (ou le module si il n'y a pas de section), l'option est restaurée à sa valeur précédente au sortir de la section. - Set/Unset ... survit aux sections mais pas aux modules. - Global Set/Unset ... survit aux sections et aux modules. Il y a une légère source d'incompatibilité là, Set avait le comportement de Local Set. Ça n'apparaît pas dans la lib standard, mais sait-on jamais. Les étapes suivantes : - Supprimer la notion d'option asynchrone, je n'en vois vraiment pas l'intérêt. Changer le type de retour de declare_option à unit aussi serait probablement une bonne idée. - Ajouter le support Local/Global à d'autres commandes sur le même modèle. Conflicts: parsing/g_vernac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12280 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-14Added profile.cmo in grammar.cma so that any functions in one of theherbelin
files embedded in grammar.cma can be profiled with the Profile module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12279 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-14Tried to make F1 documentation tool working in CoqIDE.herbelin
In trunk: New strategy for compiling and finding index_url.txt. After all, this file is not specific to CoqIDE but to the documentation. Hence, it seems better to install it close to the documentation. If the documentation is locally installed, it is easy to find the file index_url.txt but what to do if the documentation is remote? We would need a http getter. Does this mean we have to rely on wget or so? In the absence of answer to this question, it seems reasonable, first to assume the doc to be locally installed, second to have a local copy of index_url.txt ready in the installation directory of CoqIDE. Also added an "automatic" field in the CoqIDE url preference to prevent the user to have to update his preference file every time a new version of Coq is out and the link to the doc change. In 8.2: Added a minima the installation of index_urls.txt but the user will have to update its preferences because the links "http://coq.inria.fr/doc/Reference-Manual010.html#..." do not longer exist. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12278 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
only used to allow a module to be ended before the summaries were restored what can be solved by moving upwards the place where the summaries are restored). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12275 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-13Made unification patch 12268 even more ad hoc (if evars remain in aherbelin
term, its type is not the smallest one - actually, we would have to reduce the term too but it would be more costly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12274 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-11Ensures that let-in's in arities of inductive types work well. Maybe notherbelin
very useful in practice but as soon as let-in's were not forbidden in the internal data structure, better to do it. Moreover, this gets closer to the view were inductive definitions are uniformly built from "contexts". (checker not changed!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12273 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-11Ajout des .annot dans le .gitignore.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12272 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-11Fixed extra space in printing notation { x & P } + minor other thingsherbelin
(shorter proof of O_S in trunk + typo). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12271 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-11Infix (r12268 continued)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12270 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-11Add support for "Infix ... := constr" instead of just "Infix ... := ref".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12269 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-11Relatively ad hoc fix to an ill-typed instantiation bug in typeherbelin
inference (see file failure/evar1.v) + fix of some CUMUL problems that were in the wrong direction. We assume for the fix that ill-typed unification problems come from subtyping where we don't know yet if a coercion has to be inserted or not, and hence are of the CUMUL form. More on suspending problems of the form ?n <= Type or Prop <= ?n has to be done yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12268 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-07Fixed incorrect optimization in Prettyp.pr_located_qualid introducedherbelin
in commit r12265. Add a few synonyms back in Libnames/Nameops to maintain some minimal compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12267 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-06Cleaning of Nametab continued + fixed a compilation bug in previous commit.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12266 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
(uniformisation of function names, classification). One of the most visible change is the renaming of section_path into full_path (the use of name section was obsolete due to the module system, but I don't know if the new name is the best chosen one - especially it remains some "sp" here and there). - Simplification of the interface of classify_object (first argument dropped). - Simplification of the code for vernac keyword "End". - Other small cleaning or dead code removal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-06Move out JMeq of subst for compatibility (it affects e.g. theherbelin
compilation of Grenoble/ATBR). Add subst' for subst extended with JMeq (maybe an option would be better??). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12264 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-05changed deprecated setoid into relationamahboub
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12263 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-04- Add more precise error localisation when one of the application failsherbelin
in a chain of apply or apply-in. - Improved comments on the notions of permutation used in the library (still the equality relation in file Permutation.v misses the property of being effectively an equivalence relation, hence missing expected properties of this notion of permutation). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12261 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-04Fixed subst failing when a truly heterogeneous JMeq hyp is in theherbelin
context (problem introduced in r12259) + improved backward compatibility in hippatern.mli (wrt r12259). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12260 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-03Added "etransitivity".herbelin
Added support for "injection" and "discriminate" on JMeq. Seized the opportunity to update coqlib.ml and to rely more on it for finding the equality lemmas. Fixed typos in coqcompat.ml. Propagated symmetry convert_concl fix to transitivity (see 11521). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-02Improved parameterization of Coq:herbelin
- add coqtop option "-compat X.Y" so as to provide compatibility with previous versions of Coq (of course, this requires to take care of providing flags for controlling changes of behaviors!), - add support for option names made of an arbitrary length of words (instead of one, two or three words only), - add options for recovering 8.2 behavior for discriminate, tauto, evar unification ("Set Tactic Evars Pattern Unification", "Set Discriminate Introduction", "Set Intuition Iff Unfolding"). Update of .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-02Fixed a typo in "info" for tactic "right".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12257 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-01csdpcert + unixfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12256 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-31addition of lia.cache - csdp.cache is now handled by micromega not csdpcertfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12255 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-30micromega : Better parsing of formulae - smaller proof terms for Z - ↵fbesson
redesign of proof cache git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12254 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-30psatz Z -> psatz Z 1fbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12253 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-30Git ignore filesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12252 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-30For git users, a global .gitignore fileletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12251 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-24OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArithletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12250 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-24List: add a iff-based lemma about In and ++letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12249 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-24Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"letouzey
I wonder how many of us were aware of the existence of such syntax ;-) Anyway, it is now subsumed by "rewrite by". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12248 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-22Better comparison functions in OrderedTypeExletouzey
The compare functions are still functions-by-tactics, but now their computational parts are completely pure (no use of lt_eq_lt_dec in nat_compare anymore), while their proofs parts are simply calls to (opaque) lemmas. This seem to improve the efficiency of sets/maps, as mentionned by T. Braibant, D. Pous and S. Lescuyer. The earlier version of nat_compare is now called nat_compare_alt, there is a proof of equivalence named nat_compare_equiv. By the way, various improvements of proofs, in particular in Pnat. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12247 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-20Use unfold directly in unfold_equations. Fixes test-suite.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12246 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-20Use camlp4 to accept some specific non-exhaustive patterns in groebnerletouzey
The camlp4 extension "refutpat" provides a syntax let* for pattern that are non-exhaustive on purpose (e.g. let* x::l = foo in ...). A Failure is raised if the pattern doesn't match the expression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12245 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-20Move some examples for groebner into a test-suite fileletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12244 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-20Typo in a commentletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12243 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-15- Granted wish #2138 (support for local binders in syntax of Record fields).herbelin
- Add tests related to commits 12229 (bug #2117) and 12241 (bug #2139). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12242 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-15- Fixing bug #2139 (kernel-based test of well-formation of eliminationherbelin
predicate called from proof refiner was failing because it was not aware of evars instantiation; I added a nf_evar in 8.2 branch but for the trunk, I propose to remove the elimination predicate well-formation test; we therefore assume that tactics build correct elimination predicates in Case, is it not too much demanding?). - Seized the opportunity to remove dead kernel code about non dependent elimination predicates (all predicates are stored dependent by default since a few years now). - Anecdotic complement to commit 12229 (removal of obsolete comment). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12241 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-14Simplify eauto and fix it for compatibility, allowing full delta duringmsozeau
unification for exact hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12239 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-09Use the proper unification flags in e_exact. This makes exact fail a bitmsozeau
more often but respects the spec better. The changes in the stdlib are reduced to adding a few explicit [unfold]s in FMapFacts (exact was doing conversion with delta on open terms in that case). Also fix a minor bug in typeclasses not seeing typeclass evars when their type was a (defined) evar itself. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12238 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-09Allow coqdoc comments inside definition bodies.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12237 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-09Correction bug 2134.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12235 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Fixed bug #2116 ("simpl" created ill-typed term while acceptingherbelin
inverting a recursive constant with dependent K-parameters). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12233 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Don't use recent ocaml tolerance for pattern "ProjectVar _" whenherbelin
ProjectVar is a constant constructor (anyway, use of _ for constant constructor was here by mistake). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12232 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Simplify addition of hints to a hint_db. Rebuild the dnet associatedmsozeau
with it when the transparent state changes and not only when [Hint Unfold] is added. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12231 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Use user-given implicits from the arity in inductive definitions.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12230 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 18:08:41 +0000