Permalink
Switch branches/tags
Nothing to show
Commits on Oct 12, 2012
  1. Fix two remainining calls to merge_constraints that were not catched …

    …in case
    
    of -warn-universe-inconsistency.
    mattam82 committed with Oct 5, 2012
  2. Changed the behavior of -relevant-equality so that Set is not

    considered small, in the sense that a type in Set does not
    get equality in Prop. This is the desired behavior for the
    homotopy interpretation where Set cannot be interpreted, say,
    as the intersection of hset and the lowest universe.
    
    It would still be good to make absence of -relevant-equality
    contaminant so that we cannot accidentally use the standard
    library when the option is present.
    
    And yes, there is no hope of compiling the standard library
    with this option turned on.
    andrejbauer committed with Oct 3, 2012
  3. Patch by Hugo Herbelin.

     Added an option -relevant-equality to Coq which makes the
     logic compatible with a model such as the univalent model
     where proofs of equality are informative as soon as they
     involve elements in some Type level. This has an effect on
     the level in which universe-polymorphic inductive types are
     placed, which can be higher than w/o the option, and on
     which singleton eliminations are allowed, which can be less
     than w/o the option.
    
    How indices contribute:
    - Indices in A:Prop do not contribute to the level of an inductive nor
      on whether singleton elimination is allowed or not.
    - We chose to interpret Set as a sort in which proofs of equality are
      irrelevant (i.e. a sort in which Streicher's K holds). Hence indices
      in A:Set do not contribute to the level of the inductive. In
      particular, elimination from "Inductive eq (A:Set) (a:A) : A -> Prop
      := refl : eq A a a." is unrestricted. Similarly, the default lower
      level of polymorphic "Inductive eq (A:Set) (a:A) : A -> Type := refl
      : eq A a a." is Prop.
    - Indices in A:Type contribute to raising the level of a
      universe-polymorphic type. E.g. "Inductive eq (A:Type (* u *) ) (a:A) :
      A -> Type := refl : eq A a a." is in "Type (* u *)". Similarly,
      singleton elimination is forbidden from "Inductive eq (A:Type) (a:A)
      : A -> Prop := refl : eq A a a.".
    
    Remarks:
    - The modification applies uniformly to all inductive types with
      indices, not only those resembling equality.
    - The standard library stops to compile when the option is activated.
    - We could have been finer, and only restrict singleton eliminations
      dynamically depending on the level of the effective sort
      used. E.g. with "Inductive eq (A:Type) (a:A) : A -> Prop := refl :
      eq A a a.", we could have allowed "eq nat" to be eliminable to every
      sorts (because nat can be finally be put in Set and not in some
      higher Type). With this, a larger amount of the standard library
      could be compiled by reasoning in Set rather than in Type.
      However, this is not implemented.
    mattam82 committed with Oct 3, 2012
  4. Add a command line option to turn universe inconsistencies into warni…

    …ngs,
    
    not adding the "offending" constraints. Cannot be turned on to errors again.
    mattam82 committed with Sep 28, 2012
Commits on Oct 8, 2012
  1. fix r15860 : no slash after $(COQLIB)

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15882 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 8, 2012
Commits on Oct 6, 2012
  1. restore compatibility with camlp5 < 6.00

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15881 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  2. Coqmktop: a misplaced Filename.quote prevented temp file cleanup

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15880 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  3. Turn mltop.ml4 into a regular ocaml file

     The IFDEF's in mltop.ml4 were there to support platforms with
     a native ocaml compiler but no dynlink.cmxa, a situation that
     should be pretty rare in the Coq community nowadays (playing
     with coqtop on ARM, anyone ?). So we now refuse to build
     a native coqtop unless dynlink.cmxa exists (cf ./configure),
     and we explain how to create a dummy one if necessary
     (cf dev/dynlink.ml). This way, we can clean-up mltop.ml,
     and remove ugly special rules in Makefile and myocamlbuild
    
     NB: I checked that this shouldn't have any impact on Coq's
     debian packages on exotic architectures (arm, mips, ...),
     since apparently on these architectures no ocamlopt at all
     are shipped, and coq packages are already byte-only
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15879 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  4. ocamlbuild simplifications

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15878 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  5. Minor fix in the ./build wrapper for ocamlbuild

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15877 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  6. no need for camlp4 cma's in coq misc tools

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15876 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  7. still some more dead code removal

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  8. remove useless hidden_flag in TacMutual(Co)Fix

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15874 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  9. cosmetic concerning interp of TacShowHyps

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15873 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  10. remove Refiner.abstract_tactic and similar

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15872 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  11. remove -rectypes except for term.ml

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15871 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  12. remove dumptree.ml4

     This file was providing the "Dump Tree" command to display
     the state of a proof in XML. This command has been broken since
     the integration of Arnaud's proof engine. Nobody cared enough
     to adapt this to the new framework, moreover the trend is
     rather now to use the xml-base dialog mode of coqtop,
     so I simply remove this obsolete code.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15870 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  13. Adapt pieces of code needing -rectypes

     * in Matching and Tacinterp : ad-hoc types for encoding matching
       result and "next" continuation
    
     * in Class_tactics, occurrences of types such as
        "type t = (foo * (unit->t) option"
       have been specialized to something like
         type t = TNone | TSome of foo * (unit -> t)
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15869 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  14. avoid using rectypes in dnet.ml

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15868 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  15. avoid using rectypes in nametab.ml

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15867 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  16. Tacexpr: revised version that doesn't need -rectypes

     For that, gen_atomic_tactic_expr and gen_tactic_expr are now
     mutually recursive
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15866 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  17. Clean-up : removal of Proof_type.tactic_expr

     This instance of gen_tactic_expr was used only to decorate
     tactics via Refiner.abstract_tactics and alii, but these
     expressions are now ignored by the new proof-engine (no "info"...).
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15865 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  18. Proof_type: rule now degenerates to prim_rule

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15864 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  19. Clean-up : no more Proof_type.proof_tree

     Btw, remove unused code in the xml plugin and in Tactic_printer
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15863 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
  20. Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box

     Nested was never constructed, while the notion of abstract_tactic_box
     is obsolete (cf. Refiner.abstract_tactic).
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15862 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 6, 2012
Commits on Oct 5, 2012
  1. Fix a confusion between types of locations in an untyped part of the …

    …parser
    
    after the migration of compat.ml4
    
     This was leading to huge positions written to .glob files, making
     coqdoc loop forever.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15861 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 5, 2012
  2. Repair the configure after Hugo's last "repair" ;-)

     Ok, I wasn't aware of the funny behavior of cd in presence of $CDPATH.
     But the last "repair" was worse, trying to write into non-existing file
     theories/config/coq_config.ml
    
     Things should be better now:
    
     * no more Coq_config.theories_dirs at all, since it was completely unused :-)
    
     * concerning Coq_config.plugins_dirs, we list them without any "cd" into plugins,
       hence keeping the "plugins/" part in their paths, and adapt accordingly
       the only use (!) of plugins_dirs, in coq_makefile
    
     Please run ./configure again after upgrading to this commit
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15860 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 5, 2012
  3. coqtop -time : display per-command timings

    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15859 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 5, 2012
  4. More accurate timings for "Time foo"

     The elapsed time in seconds was computed via a difference of Unix.time(),
     but these Unix.time() aren't precise enough (just a number of seconds),
     and a difference is hence even less precise.  We now use Unix.gettimeofday,
     and round the time difference to the millisecond.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15858 85f007b7-540e-0410-9357-904b9bb8a0f7
    letouzey committed Oct 5, 2012
Commits on Oct 4, 2012
  1. Revert r15851 "En cours pour bug 2836".

    Sorry, was committed mistakenly.
    
    This reverts commit e9cb84af469519b824899c047eed1fed2f8d5af6.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15857 85f007b7-540e-0410-9357-904b9bb8a0f7
    herbelin committed Oct 4, 2012
  2. Revert "En cours pour 'generalize in clause' et 'induction in clause'"

    Sorry, was committed mistakenly.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15856 85f007b7-540e-0410-9357-904b9bb8a0f7
    herbelin committed Oct 4, 2012
  3. Repaired configure damaged in r15748 for those bash users which have

    CDPATH variable set. Indeed, command cd is verbose when CDPATH is set,
    what would introduce garbage in the generated file config/coq_config.ml.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15855 85f007b7-540e-0410-9357-904b9bb8a0f7
    herbelin committed Oct 4, 2012
  4. Suggest to use clean rather than archclean before recompiling.

    For instance, generated files depend on whether configuration is done
    with dynlink or not and they should be cleaned.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15854 85f007b7-540e-0410-9357-904b9bb8a0f7
    herbelin committed Oct 4, 2012