aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2009-10-06Fixed installation of Coqide interface/library files (bug #2147).gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12376 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-06Relaxed error severity when encountering unknown library objects or tacticgmelquio
extensions. This makes it possible to load .vo compiled with a nonstandard toplevel, e.g. ssreflect, which defines new tactics and new hint databases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12375 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-05Correctly do backtracking during type class resolution even if only newmsozeau
existentials are generated (at last!). The code simply keeps failure continuations and apply them if needed. Fix bottomup and topdown rewrite strategies that looped. Use auto introduction flag for typeclass instances as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12374 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-05Revert "kills the old backtracking framework and replaces it with"vgross
This reverts commit 33545cc88bf4b4e19b222afd2d1d264bcba97838. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12373 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-04Changed the way to support compatibility with previous versions.herbelin
Compatibility version is now a global parameter that every feature can individually browse. This avoids having to keep the names of options synchronous in their respective files and in now-removed file coqcompat.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12372 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-04Removal of trailing spaces.serpyc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12371 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-04Some new lemmas on max and min and a fix for a wrongly stated lemma in r12358.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12370 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-03Fixed small name freshness bug in Functional Scheme ("Heq" name washerbelin
not refreshed late enough). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12369 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-03A few additions in Min.v.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12368 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-03Added option "Unset Dependent Propositions Elimination" to protectherbelin
against the incompatibilities introduced by making "destruct" working on dependent propositions (incompatibilities come from uses of destruct in Ltac definitions such as "destruct_conjs"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12367 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-29Add support for Local Declare ML Moduleglondu
Instead of failing with some obscure error message *after* loading the module, accept Local Declare ML Module with the usual semantics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12366 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-29Remove legacy export_* functionsglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12365 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-29kills the old backtracking framework and replaces it withvgross
ProofGeneral-like "Backtrack". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12364 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-28Fix the stdlib doc compilation + switch all .v file to utf8letouzey
1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v In fact coqdoc was trying to recognize the end of a _emphasis_ and hence inserted a bogus }. For the moment I've enclosed the phrase with [ ], but this emphasis "feature" of coqdoc seems _really_ easy to broke. Matthieu ? 2) By the way, this Library document was made from latin1 and utf8 source file, hence bogus characters. All .v containing special characters are converted to utf8, and their first line is now mentionning this. (+ killed some old french comments and some other avoidable special characters). PLEASE: let's stick to this convention and avoid latin1, at least in .v files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-28Applied patches from BSD/pkgsrc maintainer, so that Coq compiles out-of-the-box.gmelquio
- Removed unneeded bashisms. (sh and dash are fine with the current build system.) - Removed workaround for camlp4.opt on BSD. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12362 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-20 18:45:38 +0000