aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-03-01various corrections in invfun due to a modification in inductionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15008 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-29Univ: a faster is_leq test used when possibleletouzey
Let's reintroduce the idea of stopping the graph traversal as soon as a LE arc has been found, but this time we do so only when we're not interested by the LT/LE distinction. This way, we should remain correct but avoid largly the time penalty induced by the last fix on univ.ml: the +30% on contrib Container is almost gone, let's hope it'll be the same with Ssreflect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15007 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-29correcting a little bug in invfun.mljforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15005 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-29correction of bug 2457jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15004 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-29Fix compilation of Constrintern...pboutill
I love being push under presure to commit and do not try my fixup ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15003 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-29RefMan update about match syntax.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15002 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-29In the syntax of pattern matching, the arguments of the inductive in the "in"pboutill
clause can be any pattern. It is expanded as a match in the return clause. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15001 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-29In the syntax of pattern matching, "in" clauses are patterns.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15000 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-29Vector: missing injection lemmas and better impossible branchespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14999 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-29Bug 2703: send stdout dump to coqide when an error occurs.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14998 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-29Coq_makefile: Add of extra options by defaultpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14997 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-27Univ: correct compare_neq (fix #2703)letouzey
The earlier version was a bit too quick to answer <= while strict constraints could still appear from remaining universes to explore. Typical situation: compare u v when u <= v and u <= w < v. Encountering u <= v isn't enough to conclude yet... This means that kernels from r13719 to now in trunk, and from r13735 to now in 8.3 (including 8.3pl{1,2,3}) couldn't accurately detect universe inconsistencies, leading to potential proofs of False! Oups, sorry... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14993 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-23Implement the substitution function for global options. Fixes anomaly in ↵msozeau
ssreflect compilation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14991 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-22Ide: sentences found by find_phrase_starting_at should be nonempty (fix #2683)letouzey
In addition to #2683, this also prevent Vernac.End_of_input exceptions when a buffer ends with one of the new delimiters -+*{}. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14989 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-20Use a heuristic to not simplify equality hypotheses remaining after ↵msozeau
dependent induction if they don't look really trivial. We still are making a choice though. Fixes bug #2712. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14988 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-20- changing minimal version for OCaml: Coq uses Filename.dirsep that is ↵notin
available from OCaml 3.11.2 (see bug #2707) - fixing outdated address for Coq Club git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14987 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-20Correct application of head reduction.msozeau
Fix a regression in subtac_pretyping, avoiding application of bidirectional application checking in case the return type is a subset (bad interaction with typeclass overloading). Should be done only on constructor applications. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14985 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-18Document the [unify] tactic.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14984 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-16Fix handling of space after "Notation" or "where", add missing keywords.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14983 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-15Avoid retrying uncessarily to prove independent remaining obligations in ↵msozeau
Program. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14982 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-15Avoid unnecessary normalizations w.r.t. evars in Program.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14981 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-15Fix in evarutil: add a conversion problem for ?x ts = ?x us only if ts and ↵msozeau
us are not convertible git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14980 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-14In [reflexivity], [symmetry] etc, use the type found by looking at the ↵msozeau
relation as the carrier instead of the first argument's type (plays nicer with coercions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14979 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-14- Fix dependency computation in eterm to not consider filtered variables.msozeau
- Fix handling of evar map in Program coercion code that could forget some new declarations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14978 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-14Arguments supports extra notation scopesgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14977 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-07Additional comment on Focus Conditions.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14975 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-07Documentation for Grab Existential Variables.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14974 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-07A "Grab Existential Variables" to transform the unresolved evars at the end ↵aspiwack
of a proof into goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14973 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-07Typo in comments.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14972 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-03correcting inversion in list of generated tcc of Functionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14967 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-02More information returned by coqtop about its internal state. Hopefully ↵ppedrot
we'll manage to get rid of the own stack of coqide. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14965 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-01Fix unblocking code in dependent destruction due to zeta being used in ↵msozeau
unfold now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14964 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-01Corrected a careless cut-and-paste in Gallina description which dated back ↵ppedrot
to 2003. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14963 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-01Debugger vs tracer: Two different behaviors wrt printing: The debuggerherbelin
runs in separate process. It has no access to the global env and it should not request it. The tracer runs in the same process as Coq and has full access to the global env and to regular pretty-printing of global names. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14958 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-01Improved synchronisation of stdlib index page with current library state.herbelin
- Made generation of index page fail if a file is missing in list or listed but unbound in existing theories - Added a file hidden-files to optionally list library files not to show in the index page (though it is currently empty) - Added directory Unicode (why not to have it after all?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14957 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-31Revert "Tentative to fix bug #2628 by not letting intuition break records. ↵msozeau
Might be too much of a backwards-incompatible change" Indeed it is breaking too many scripts. This reverts commit 47e9afaaa4c08aca97d4f4b5a89cb40da76bd850. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14956 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-31index-list.html.template: add missing filespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14955 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-31Fix consequence of pp bugfix in testsuitepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14954 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-31Makefile.build: add targets install-devfiles and install-ide-devfilespboutill
It makes special rules for files useless when the Ocaml used to compile coq is not installed git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14953 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-31Bug #2041: unfold at betaiotaZETA normalize like unfoldpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14952 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-31Fix camlp4 compilationpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14951 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-30Added an pattern / occurence syntax for vm_compute.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14950 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-28Tentative to fix bug #2628 by not letting intuition break records. Might be ↵msozeau
too much of a backwards-incompatible change git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14949 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-28Fix simplification of ind. hyps., recognized by a [block] in their type (bug ↵msozeau
#2674) and properly clear [block] at end of simplification (bug #2691). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14948 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-27Printing bugs with match patterns:herbelin
- namegen.ml: if a matching variable has the same name as a constructor, rename it, even if the conflicting constructor name is defined in a different module; - constrextern.ml: protect code for printing cases as terms are from requesting info in the global env when printers are called from ocamldebug since the global env is undefined in this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14947 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-26Fail: discard the effects of a successful command (fix #2682)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14945 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-26Add support for plugin initialization functiongareuselesinge
Plugins can call add_known_plugin instead of add_known_module to specify an initialization function. That function is granted to be called after the system initialization (in case of static linking) and every time their are "loaded" with Declare ML Module (even if the .cmo or .cmxs is actually loaded only once since OCaml is unable to unload dynamically linked modules). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14944 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-25Check for unresolved evars in textual order of the params and fields ↵msozeau
declarations (fixes bug #2278). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14943 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-23Fix bug #2483: anomaly raised due to wrong handling of the evars state.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14942 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-01-23Fix typeclass resolution error message which included goal evars (bug #2620).msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14941 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 23:26:21 +0000