Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Commits on Jun 28, 2012
  1. @ppedrot

    Fixing previous commit.

    ppedrot authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15498 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. @ppedrot

    Fixing info_auto / info_trivial display.

    ppedrot authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15497 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jun 22, 2012
  1. @ppedrot

    Added an indirection with respect to Loc in Compat. As many [open Com…

    ppedrot authored
    …pat]
    
    were closed (i.e. the only remaining ones are those of printing/parsing).
    Meanwhile, a simplified interface is provided in loc.mli.
    
    This also permits to put Pp in Clib, because it does not depend on
    CAMLP4/5 anymore.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jun 19, 2012
  1. Fix bug #2790: wrong handling of Set -> Prop -> Prop products in seto…

    msozeau authored
    …id rewriting.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15452 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jun 4, 2012
  1. @ppedrot

    Replacing some str with strbrk

    ppedrot authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15422 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. Forward-port fixes from 8.4 (15358, 15353, 15333).

    msozeau authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15418 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Jun 1, 2012
  1. @ppedrot

    More cleaning

    ppedrot authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15414 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. @ppedrot

    Cleaning Pp.ppnl use

    ppedrot authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15413 85f007b7-540e-0410-9357-904b9bb8a0f7
  3. @ppedrot

    Getting rid of Pp.msgnl and Pp.message.

    ppedrot authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
  4. Let's try to avoid generating induction principles for records (wish …

    letouzey authored
    …#2693)
    
     Since record cannot be recursive, induction principles for them are
     just wasted ressources. With this patch, we turn off there generation
     by default. The flag "Set/Unset Record Elimination Schemes" allows
     to start producing them again.
    
     For compatibility, we adapt "induction" and similar tactics that
     rely on the existence of induction principles : on a record,
     "induction" is now silently converted into "destruct".
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15411 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on May 31, 2012
  1. @pirbo

    tactic is_fix, akin to is_evar, is_hyp, is_ ... family

    pirbo authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15406 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on May 30, 2012
  1. @ppedrot

    Getting rid of Pp.msg

    ppedrot authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. @ppedrot

    More uniformisation in Pp.warn functions.

    ppedrot authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on May 29, 2012
  1. remove many excessive open Util & Errors in mli's

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. No need to have Refine amongst Hightactics.cm*a

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15388 85f007b7-540e-0410-9357-904b9bb8a0f7
  3. place all files specific to camlp4 syntax extensions in grammar/

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15387 85f007b7-540e-0410-9357-904b9bb8a0f7
  4. global_reference migrated from Libnames to new Globnames, less deps i…

    letouzey authored
    …n grammar.cma
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
  5. Basic stuff about constr_expr migrated from topconstr to constrexpr_ops

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15382 85f007b7-540e-0410-9357-904b9bb8a0f7
  6. slim down a bit genarg.ml (pr_intro_pattern forgotten there)

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15380 85f007b7-540e-0410-9357-904b9bb8a0f7
  7. Pattern as a mli-only file, operations in Patternops

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15376 85f007b7-540e-0410-9357-904b9bb8a0f7
  8. New files intf/constrexpr.mli and intf/notation_term.mli out of Topco…

    letouzey authored
    …nstr
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
  9. Glob_term now mli-only, operations now in Glob_ops

    letouzey authored
    Stuff about reductions now in genredexpr.mli, operations in redops.ml
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 85f007b7-540e-0410-9357-904b9bb8a0f7
  10. Tacexpr as a mli-only, the few functions there are now in Tacops

    letouzey authored
     NB: former Tacexpr.no_move is now Tacexpr.MoveLast
      (when introducing, intro with no move is intro as last)
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15373 85f007b7-540e-0410-9357-904b9bb8a0f7
  11. locus.mli for occurrences+clauses, misctypes.mli for various little t…

    letouzey authored
    …hings
    
     Corresponding operations in locusops.ml and miscops.ml
    
     The type of occurrences is now a clear algebraic one instead of
     a bool*list hard to understand.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
  12. Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
  13. Vernacexpr is now a mli-only file, locality stuff now in locality.ml

    letouzey authored
     Adds a directory ./intf for pure interfaces.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on May 15, 2012
  1. Intuition: temporary(?) restore the unconditional unfolding of not

    letouzey authored
     Let's check tomorrow the impact on contribs: are the recent build
     failures related to the "not" unfolding stategy or to the new
     handling of conjonction-like constructors ?
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15330 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Apr 23, 2012
  1. remove undocumented and scarcely-used tactic auto decomp

    letouzey authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15241 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Apr 18, 2012
  1. @aspiwack

    Corrects a (very) longstanding bug of tactics. As is were, tactic exp…

    aspiwack authored
    …ecting
    
    constr as argument (rather than openconstr) assumed that the evar_map
    output by pretyping was irrelevant as the final constr didn't have any evars.
    However, if said constr was defined using pre-existing evars from the
    context, the evars may be instantiated by pretyping, hence dropping the
    output evar_map led to inconsistent proof terms.
    
    This fixes bug #2739 ( https://coq.inria.fr/bugs/show_bug.cgi?id=2739 ).
    Thanks Arthur for noticing it.
    
    Note: change still has the bug, because more serious issues interfered with
    my fix.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15207 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. @aspiwack

    Adds the openconstr entry for tactic notations.

    aspiwack authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15206 85f007b7-540e-0410-9357-904b9bb8a0f7
  3. @aspiwack

    Better error message in tactic notations.

    aspiwack authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15203 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Apr 17, 2012
  1. Remove the Dp plugin.

    gmelquio authored
    Why2 has not been maintained for the last few years and the Why3 plugin should
    be a suitable replacement in most cases.
        
    Removed tactics: simplify, ergo, yices, cvc3, z3, cvcl, harvey, zenon, gwhy.
    Removed commands: Dp_hint, Dp_timeout, Dp_prelude, Dp_predefined, Dp_debug,
      Dp_trace.
        
    Note that the "admit" tactic was actually provided by the Dp plugin. It has
    been moved to extratactics.ml4.
    
    Ported from v8.4 r15186.
    
    
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15189 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Apr 15, 2012
  1. Fixing tauto "special" behavior on singleton types w/ 2 parameters (b…

    herbelin authored
    …ug #2680).
    
    - tauto/intuition now works uniformly on and, prod, or, sum, False,
      Empty_set, unit, True (and isomorphic copies of them), iff, ->, and
      on all inhabited singleton types with a no-arguments constructor
      such as "eq t t" (even though the last case goes out of
      propositional logic: this features is so often used that it is
      difficult to come back on it).
    - New dtauto and dintuition works on all inductive types with one
      constructors and no real arguments (for instance, they work on
      records such as "Equivalence"), in addition to -> and eq-like types.
    - Moreover, both of them no longer unfold inner negations (this is a
      souce of incompatibility for intuition and evaluation of the level
      of incompatibility on contribs still needs to be done).
    
    Incidentally, and amazingly, fixing bug #2680 made that constants
    InfA_compat and InfA_eqA in SetoidList.v lost one argument: old tauto
    had indeed destructed a section hypothesis "@StrictOrder A ltA@
    thinking it was a conjunction, making this section hypothesis
    artificially necessary while it was not.
    
    Renouncing to the unfolding of inner negations made auto/eauto
    sometimes succeeding more, sometimes succeeding less. There is by the
    way a (standard) problem with not in auto/eauto: even when given as an
    "unfold hint", it works only in goals, not in hypotheses, so that auto
    is not able to solve something like "forall P, (forall x, ~ P x) -> P
    0 -> False". Should we automatically add a lemma of type "HYPS -> A ->
    False" in the hint database everytime a lemma ""HYPS -> ~A" is
    declared (and "unfold not" is a hint), and similarly for all unfold
    hints?
    
    At this occasion, also re-did some proofs of Znumtheory.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15180 85f007b7-540e-0410-9357-904b9bb8a0f7
  2. In "intro until" and its applications, be consistent when reduction is

    herbelin authored
    used or not before trying to introduce.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15175 85f007b7-540e-0410-9357-904b9bb8a0f7
Commits on Apr 12, 2012
  1. @pirbo

    Remove print call that do not use the pp mechanism

    pirbo authored
    Signed-off-by: Edward Z. Yang <ezyang@mit.edu>
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15148 85f007b7-540e-0410-9357-904b9bb8a0f7
Something went wrong with that request. Please try again.