aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2009-09-15Dont't forget to update the state or an obligation tactic assignment maymsozeau
have no effect when the module is later imported. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12332 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-15Fixed compilation error message which was no longer emacs-compliant sinceherbelin
revision 11316. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12331 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-15Stop using [obligation_tactic] from Program.Tactics as the defaultmsozeau
obligation tactic so that [Program] can work without importing anything. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12330 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-14Backtrack on the forced discharge of type class variables introducedmsozeau
by Context. Now Context has exactly the same semantics as Variables. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12329 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-14removed the double-click / proof hiding association.vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12328 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-14tags refactoringvgross
all tags are isolated in tags.ml, and all tags are accessed directly, not through their names. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12327 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-14- Addition of "Reserved Infix" continued.herbelin
- Tried an extension of the lexer that supports keywords starting with a letter w/o being an ident (e.g. 'U+'). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12326 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-13- Inductive types in the "using" option of auto/eauto/firstorder areherbelin
interpreted as using the collection of their constructors as hints. - Add support for both "using" and "with" in "firstorder". Made the syntax of "using" compatible with the one of "auto" by separating lemmas by commas. Did not fully merge the syntax: auto accepts constr while firstorder accepts names (but are constr really useful?). - Added "Reserved Infix" as a specific shortcut of the corresponding "Reserved Notation". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12325 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-11Addendum to revision 12323; update Makefile.common after removal ofherbelin
ExternalProvers.tex in revision 12320. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12324 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
string in most commands expecting a global name (e.g. 'Print "+"' for an infix notation or 'Print "{ _ } + { _ }"' for a misfix notation, possibly surrounded by a scope delimiter). Support for such smart globals in VERNAC EXTEND to do. Added a file smartlocate.ml for high-level globalization functions. Mini-nettoyage metasyntax.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12323 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-11Add doc of [Context] vernacular.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12322 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-11Added the following lemmas to homogenize Reals a bit:gmelquio
- Rmult_eq_compat_r, Rmult_eq_reg_r, Rplus_le_reg_r, Rmult_lt_reg_r, Rmult_le_reg_r (mirrored variants of the existing _l lemmas); - minus_IZR, opp_IZR (Ropp_Ropp_IZR), abs_IZR (mirrored Rabs_Zabs); - Rle_abs (RRle_abs); - Zpower_pos_powerRZ (signed variant of Zpower_nat_powerRZ). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12321 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-11Removed Gappa from the external provers supported by the dp plugin. Tactic ↵gmelquio
gappa has been supported for some time in an external package. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12320 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-11- Resolve type class constraints before trying to find unresolvedmsozeau
obligations in [Program Fixpoint]. - Add maximal implicits for pairs in [Program.Syntax]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12319 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-10Fixes for toc depth handling and handling of substitles from Chris Casinghino.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12318 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-10Misc fixes:msozeau
- better implicits for [antisymmetry] - don't throw away implicit arguments info when doing [Program Definition : type.] - add standard debugging tactics to print goals/hyps in Program. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12317 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-10Added syntax "exists bindings, ..., bindings" for iterated "exists".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12316 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-09Allow setoid rewrite to rewrite in pattern-matching scrutinees ormsozeau
branches when constructors have no arguments, requiring the output relation of the rewrite to be leibniz equality. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12314 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-09Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsletouzey
Mostly results about Zgcd (commutativity, associativity, ...). Slight improvement of ZMicromega. Beware: some lemmas of Zdiv/ Znumtheory were asking for too strict or useless hypothesis. Some minor glitches may occur. By the way, some iff lemmas about negb in Bool.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12313 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-09Stop trying to search if the relation is declared as a [RewriteRelation]msozeau
before attempting generalized rewriting as the relation may itself be instantiated during the unification of the lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12312 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-08Update coqdoc documentation, CHANGES and add a fix for the proofbox (patchmsozeau
by Chris Casinghino). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12311 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-08Fix the bug-ridden code used to choose leibniz or generalizedmsozeau
rewriting (thanks to Georges Gonthier for pointing it out). We try to find a declared rewrite relation when the equation does not look like an equality and otherwise try to reduce it to find a leibniz equality but don't backtrack on generalized rewriting if this fails. This new behavior make two fsets scripts fail as they are trying to use an underlying leibniz equality for a declared rewrite relation, a [red] fixes it. Do some renaming from "setoid" to "rewrite". Fix [is_applied_rewrite_relation]'s bad handling of evars and the environment. Fix some [dual] hints in RelationClasses.v and assert that any declared [Equivalence] can be considered a [RewriteRelation]. Fix minor tex output problem in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12310 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-07ajout CVC3; ajout traduction des reelsmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12309 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-04Incorporate coqdoc changes by the UPenn team (B.Pierce, C. Casinghino,msozeau
M. Greenberg) and add support for interpolation to HTML output. The patch is mostly backwards-compatible, except for the CSS style which needs more readaptation. Doc for the new options will come as well. - lists have been updated substantially. In particular, multiparagraph list items are now supported and sublists work better, using an "off-side" rule. - the "--index" flag allows one to change the name of the generated index file (good since index.html has a special meaning). - the "--toc-depth <int>" flag allows one to limit how many levels are included in the toc. - the "--lib-name <string>" flag allows one to specify what libraries are called, instead of just sticking "Library" before each module name (for example, "Module" or "Chapter" might be more sensible in some contexts). Additionally "--no-lib-name" eliminates this extra title completely. - the "--lib-subtitles" flag allows one to specify subtitles for libraries. When enabled, the beginning of each file is checked for a comment of the form: (** * ModuleName : text *) and the text will be printed as a subtitle in the appropriate places. - Text can be made italic by putting it inside underscores, as in: _emphasized text_. This has the advantage of looking OK in the .v file as well. A few simple rules are followed to make sure identifiers with underscores aren't accidentally made italic. - Various changes have been made in an attempt to beautify the output, especially in html, while allowing the .v sources to look decent as well. Mostly these involve whitespace. - The coqdoc.css file has been changed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12308 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-03Add --plain-comments patch by F. Garillot, which also addsmsozeau
interpretation of [[ etc... inside (* *) comments when --parse-comments is used. Add some additional fixes from B. Pierce on formatting verbatim and the HTML Toc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12307 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-03Support globality flag properly for "Add Morphism foo : foo_mor" syntax.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12306 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-03Remove unnecessary redefinitions of [Fix_sub] and [Fix_F_sub], asmsozeau
suggested by Francois Pottier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12305 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-02Postpone checking of Local/Global to allow grammar extensions to use itmsozeau
too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12304 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-02Stop unnecessary use of lazy values for constraints, simplifyingmsozeau
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
2009-09-02Hack to correctly get ill-formed rec body exceptions even msozeau
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
2009-08-31Fix notation for ~x in theories/Unicode/Utf8.vglondu
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
2009-08-29Fix minor spelling errorglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12300 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-28update for why 2.19marche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12297 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-27Correction bug 2140.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12296 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-25git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 ↵fbesson
85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-25Delegate _all_ doc targets to stage2lmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12293 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-25install-doc* are PHONYlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12292 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-24New tactic to rewrite decidability lemmas when one knows which sideherbelin
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
2009-08-23A new kind of automatically generated scheme "congr" for equality typesherbelin
(fixing and completing commit 12273). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12290 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-23Fix a small oversight in checker commit 12288.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12289 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-22Transfers to checker ("let"s in inductive arities + Coq root read-only).herbelin
- 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
2009-08-20new csdp cache + improved error messagefbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12287 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-20new csdp cache + improved error messagefbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12286 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-04 02:08:09 +0000