aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Remove unnecessary redefinitions of [Fix_sub] and [Fix_F_sub], asGravatar msozeau2009-09-03
| | | | | | | suggested by Francois Pottier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12305 85f007b7-540e-0410-9357-904b9bb8a0f7
* Postpone checking of Local/Global to allow grammar extensions to use itGravatar msozeau2009-09-02
| | | | | | | too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12304 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stop unnecessary use of lazy values for constraints, simplifyingGravatar msozeau2009-09-02
| | | | | | | setoid_rewrite's code. Cleanup in vernacexpr. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12303 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hack to correctly get ill-formed rec body exceptions even Gravatar msozeau2009-09-02
| | | | | | | | | | | when the environment is reset. Bug is due to the use of the imperative the_globrevtab when trying to pretty-print the terms involved which may refer to the last defined obligation which is defined in the exception's environment and not the global one anymore. Bug reported by Francois Pottier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12302 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix notation for ~x in theories/Unicode/Utf8.vGravatar glondu2009-08-31
| | | | | | | | | | | Before this change, it had used: U+2309 RIGHT CEILING ("⌉") after this change, it uses: U+00AC NOT SIGN ("¬") Patch submitted on coq-club by Samuel Bronson. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12301 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix minor spelling errorGravatar glondu2009-08-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12300 85f007b7-540e-0410-9357-904b9bb8a0f7
* update for why 2.19Gravatar marche2009-08-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12297 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 2140.Gravatar soubiran2009-08-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12296 85f007b7-540e-0410-9357-904b9bb8a0f7
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 ↵Gravatar fbesson2009-08-25
| | | | 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delegate _all_ doc targets to stage2Gravatar lmamane2009-08-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12293 85f007b7-540e-0410-9357-904b9bb8a0f7
* install-doc* are PHONYGravatar lmamane2009-08-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12292 85f007b7-540e-0410-9357-904b9bb8a0f7
* New tactic to rewrite decidability lemmas when one knows which sideGravatar herbelin2009-08-24
| | | | | | | | | | | | is true. E.g. "decide (eq_nat_dec n 0) with H" on H: n=0 |- (if eq_nat_dec n 0 then 1 else 2) = 1 returns H: n=0 |- 1 = 1 . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12291 85f007b7-540e-0410-9357-904b9bb8a0f7
* A new kind of automatically generated scheme "congr" for equality typesGravatar herbelin2009-08-23
| | | | | | | | (fixing and completing commit 12273). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12290 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a small oversight in checker commit 12288.Gravatar herbelin2009-08-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12289 85f007b7-540e-0410-9357-904b9bb8a0f7
* Transfers to checker ("let"s in inductive arities + Coq root read-only).Gravatar herbelin2009-08-22
| | | | | | | | - Support for let's in the signature of the arity of an inductive type was in the kernel part of commit 12273, - Support for binding Coq root read-only in -R option was in commit 12220. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12288 85f007b7-540e-0410-9357-904b9bb8a0f7
* new csdp cache + improved error messageGravatar fbesson2009-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12287 85f007b7-540e-0410-9357-904b9bb8a0f7
* new csdp cache + improved error messageGravatar fbesson2009-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12286 85f007b7-540e-0410-9357-904b9bb8a0f7
* adds a property on mapGravatar bertot2009-08-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12285 85f007b7-540e-0410-9357-904b9bb8a0f7
* adds lemmas on interactions between existsb, forallb, and appGravatar bertot2009-08-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12284 85f007b7-540e-0410-9357-904b9bb8a0f7
* + csdp.cacheGravatar fbesson2009-08-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12283 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise à jour du document de révision de la stdlib et déplacement de laGravatar herbelin2009-08-14
| | | | | | 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
* +Fix interface.Gravatar aspiwack2009-08-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12281 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la gestion de Local et Global pour les options (au sens deGravatar aspiwack2009-08-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Added profile.cmo in grammar.cma so that any functions in one of theGravatar herbelin2009-08-14
| | | | | | 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
* Tried to make F1 documentation tool working in CoqIDE.Gravatar herbelin2009-08-14
| | | | | | | | | | | | | | | | | | | | | | | 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
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
| | | | | | | | | | 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
* Made unification patch 12268 even more ad hoc (if evars remain in aGravatar herbelin2009-08-13
| | | | | | | 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
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
| | | | | | | | | 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
* Ajout des .annot dans le .gitignore.Gravatar aspiwack2009-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12272 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed extra space in printing notation { x & P } + minor other thingsGravatar herbelin2009-08-11
| | | | | | (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
* Infix (r12268 continued)Gravatar herbelin2009-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12270 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add support for "Infix ... := constr" instead of just "Infix ... := ref".Gravatar herbelin2009-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12269 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relatively ad hoc fix to an ill-typed instantiation bug in typeGravatar herbelin2009-08-11
| | | | | | | | | | | 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
* Fixed incorrect optimization in Prettyp.pr_located_qualid introducedGravatar herbelin2009-08-07
| | | | | | | | | 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
* Cleaning of Nametab continued + fixed a compilation bug in previous commit.Gravatar herbelin2009-08-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12266 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
| | | | | | | | | | | | | | | (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
* Move out JMeq of subst for compatibility (it affects e.g. theGravatar herbelin2009-08-06
| | | | | | | | | 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
* changed deprecated setoid into relationGravatar amahboub2009-08-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12263 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Add more precise error localisation when one of the application failsGravatar herbelin2009-08-04
| | | | | | | | | | | | 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
* Fixed subst failing when a truly heterogeneous JMeq hyp is in theGravatar herbelin2009-08-04
| | | | | | | 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
* Added "etransitivity".Gravatar herbelin2009-08-03
| | | | | | | | | | | | 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
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
| | | | | | | | | | | | | | | - 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
* Fixed a typo in "info" for tactic "right".Gravatar herbelin2009-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12257 85f007b7-540e-0410-9357-904b9bb8a0f7
* csdpcert + unixGravatar fbesson2009-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12256 85f007b7-540e-0410-9357-904b9bb8a0f7
* addition of lia.cache - csdp.cache is now handled by micromega not csdpcertGravatar fbesson2009-07-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12255 85f007b7-540e-0410-9357-904b9bb8a0f7
* micromega : Better parsing of formulae - smaller proof terms for Z - ↵Gravatar fbesson2009-07-30
| | | | | | redesign of proof cache git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12254 85f007b7-540e-0410-9357-904b9bb8a0f7
* psatz Z -> psatz Z 1Gravatar fbesson2009-07-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12253 85f007b7-540e-0410-9357-904b9bb8a0f7
* Git ignore filesGravatar herbelin2009-07-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12252 85f007b7-540e-0410-9357-904b9bb8a0f7
* For git users, a global .gitignore fileGravatar letouzey2009-07-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12251 85f007b7-540e-0410-9357-904b9bb8a0f7
* OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArithGravatar letouzey2009-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12250 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 14:15:34 +0000