aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-02-29Fix compilation of Constrintern...pboutill
2012-02-29RefMan update about match syntax.pboutill
2012-02-29In the syntax of pattern matching, the arguments of the inductive in the "in"pboutill
2012-02-29In the syntax of pattern matching, "in" clauses are patterns.pboutill
2012-02-29Vector: missing injection lemmas and better impossible branchespboutill
2012-02-29Bug 2703: send stdout dump to coqide when an error occurs.pboutill
2012-02-29Coq_makefile: Add of extra options by defaultpboutill
2012-02-27Univ: correct compare_neq (fix #2703)letouzey
2012-02-23Implement the substitution function for global options. Fixes anomaly in ssre...msozeau
2012-02-22Ide: sentences found by find_phrase_starting_at should be nonempty (fix #2683)letouzey
2012-02-20Use a heuristic to not simplify equality hypotheses remaining after dependent...msozeau
2012-02-20- changing minimal version for OCaml: Coq uses Filename.dirsep that is availa...notin
2012-02-20Correct application of head reduction.msozeau
2012-02-18Document the [unify] tactic.msozeau
2012-02-16Fix handling of space after "Notation" or "where", add missing keywords.msozeau
2012-02-15Avoid retrying uncessarily to prove independent remaining obligations in Prog...msozeau
2012-02-15Avoid unnecessary normalizations w.r.t. evars in Program.msozeau
2012-02-15Fix in evarutil: add a conversion problem for ?x ts = ?x us only if ts and us...msozeau
2012-02-14In [reflexivity], [symmetry] etc, use the type found by looking at the relati...msozeau
2012-02-14- Fix dependency computation in eterm to not consider filtered variables.msozeau
2012-02-14Arguments supports extra notation scopesgareuselesinge
2012-02-07Additional comment on Focus Conditions.aspiwack
2012-02-07Documentation for Grab Existential Variables.aspiwack
2012-02-07A "Grab Existential Variables" to transform the unresolved evars at the end o...aspiwack
2012-02-07Typo in comments.aspiwack
2012-02-03correcting inversion in list of generated tcc of Functionletouzey
2012-02-02More information returned by coqtop about its internal state. Hopefully we'll...ppedrot
2012-02-01Fix unblocking code in dependent destruction due to zeta being used in unfold...msozeau
2012-02-01Corrected a careless cut-and-paste in Gallina description which dated back to...ppedrot
2012-02-01Debugger vs tracer: Two different behaviors wrt printing: The debuggerherbelin
2012-02-01Improved synchronisation of stdlib index page with current library state.herbelin
2012-01-31Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...msozeau
2012-01-31index-list.html.template: add missing filespboutill
2012-01-31Fix consequence of pp bugfix in testsuitepboutill
2012-01-31Makefile.build: add targets install-devfiles and install-ide-devfilespboutill
2012-01-31Bug #2041: unfold at betaiotaZETA normalize like unfoldpboutill
2012-01-31Fix camlp4 compilationpboutill
2012-01-30Added an pattern / occurence syntax for vm_compute.ppedrot
2012-01-28Tentative to fix bug #2628 by not letting intuition break records. Might be t...msozeau
2012-01-28Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...msozeau
2012-01-27Printing bugs with match patterns:herbelin
2012-01-26Fail: discard the effects of a successful command (fix #2682)letouzey
2012-01-26Add support for plugin initialization functiongareuselesinge
2012-01-25Check for unresolved evars in textual order of the params and fields declarat...msozeau
2012-01-23Fix bug #2483: anomaly raised due to wrong handling of the evars state.msozeau
2012-01-23Fix typeclass resolution error message which included goal evars (bug #2620).msozeau
2012-01-23Fix for Program Instance not separately checking the resolution of evars of t...msozeau
2012-01-23Another quick hack that works this time, to handle printing of locality in Pr...ppedrot
2012-01-23Deleted the only use of BeginSubProof from the standard library.ppedrot
2012-01-23Removed a seemingly unused argument in Require of modules, introduced 10 year...ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 15:00:48 +0000