aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2009-09-27Apply "Declare Implicit Tactic" also to terms interpreted as "openherbelin
terms". Let's hope the different instantiation mechanisms (implicit tactic, type classes, information coming from the with clause, ...) will combine not to badly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12361 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-27Fixed a bug in the interaction between dEqThen and inject_at_positionsherbelin
which was disturbing inversion and sometimes making it failing in presence of dependent equalities (injection still doesn't know how to split dependent equalities, resulting in a smaller number of equalities than expected for dEqThen). [also restored inv.ml as it was before 12356 which uselessly and inadvertently modified it] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12360 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-27Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12359 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-27Add a few properties about Rmin/Rmax with replication in Zmin/Zmax.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12358 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-27Fixed error message "cannot infer the type of id" in presence ofherbelin
notations for binders (the name of the notation was mistakenly taken). This happened e.g. when using Utf8.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12357 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-27Delay the choice of eliminator in destruct/induction until we know ifherbelin
a dependent scheme is needed or not (this allows for instance "destruct H" when H is propositional and dependent in the context to work). Modest attempt to clarify the basic components used and invariants preserved when sharing the code for functional induction and for destruct/induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12356 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-27Complement to 12347 and 12348 on the extended syntax of case/elim.herbelin
Don't change the semantics of "case 1" and forbid the use of numbers to refer to non-dependent quantified hypotheses in the more general forms that are synonymous of "destruct" (don't want to commit to a syntax for non-dependent quantified hypotheses which is ambiguous and after all not so appealing: for instance, something like destruct @1, destruct #1, or destruct at 1, or destruct :(ind_pattern), meaning in the latter case the first hypothesis whose type matches ind_pattern, would have probably been better). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12355 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-26Fixed a hole in glob_tactic that allowed some Ltac code to refer toherbelin
statically unbound variables (revealed by an assert failure in Tacinterp.subst_rawconstr_and_expr). In particular, tauto's use of name "id" was bypassing the globalization phase (apparently in an safe way though). Added a new kind of anomaly usable in case an anomaly results of an unexpected exception. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12354 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-24Micromega doc : psatz Z -> psatz Z 2fbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12353 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-23Ltac doc: only variables are accepted as message_tokenglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12352 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-22Add the option to automatically introduce variables declared before themsozeau
colon in (mutual) proofs with [Set Automatic Introduction]. Fix a minor test-suite issue in ProgramWf due to new handling of the default obligation tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12351 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-22Better use of transparency information for local hypotheses: msozeau
- make hyps rigid in the dnet if they're not let-ins - use existing typeclass-related transparency information for the new hints. Make the dnet better by indexing products, lambdas and sorts too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12350 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-21Update link to "Recursive Make Considered Harmful"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12349 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-20Only one "in" clause in "destruct" even for a multiple "destruct".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12348 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-20Add "case as/in/using" and temporary "destruct" with n args.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12347 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-18micromega: better handling of exponentiation + correction of test-suite ↵fbesson
termination bug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12346 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-18- Fixed a bug in checking that implicit arguments are all correctlyherbelin
instantiated in tactics (here apply and apply in) that should not open existential goals (see Bas Spitters' coq-club mail about "exists" leaving open existentials). - Preserved the history of the evars occurring in bindings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12345 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Replace call to where_in_path by find_file_in_path in "Locate File"glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12342 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Replace unprotected call to where_in_path by find_file_in_pathglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12340 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Remove useless MonoList.vglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12339 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Remove useless Liboject.export_function fieldglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12338 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Fix typos in commentsglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12336 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Clarify documentation of ltac repeatglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12335 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-15- Tentatively made order-dependency wrt .vo files a full dependencyherbelin
of the doc (use "make QUICK=1" to shortcut it) otherwise, the compilation of the doc is re-checked only when the doc files are removed. - Fixed a typo in coqdoc.sty and a redundancy in Makefile.common . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12334 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-15Fix compilation errors due to last commit.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12333 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 06:00:30 +0000