Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Commits on Oct 6, 2012
  1. restore compatibility with camlp5 < 6.00

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

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

    letouzey authored
     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
  4. ocamlbuild simplifications

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

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

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

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

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

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

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

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

    letouzey authored
     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
  13. Adapt pieces of code needing -rectypes

    letouzey authored
     * 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
  14. avoid using rectypes in dnet.ml

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

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

    letouzey authored
     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
  17. Clean-up : removal of Proof_type.tactic_expr

    letouzey authored
     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
  18. Proof_type: rule now degenerates to prim_rule

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

    letouzey authored
     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
  20. Clean-up of proof_type.ml : no more Nested nor abstract_tactic_box

    letouzey authored
     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
Commits on Oct 5, 2012
  1. Fix a confusion between types of locations in an untyped part of the …

    letouzey authored
    …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
  2. Repair the configure after Hugo's last "repair" ;-)

    letouzey authored
     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
  3. coqtop -time : display per-command timings

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

    letouzey authored
     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
Commits on Oct 4, 2012
  1. Revert r15851 "En cours pour bug 2836".

    herbelin authored
    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
  2. Revert "En cours pour 'generalize in clause' et 'induction in clause'"

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

    herbelin authored
    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
  4. Suggest to use clean rather than archclean before recompiling.

    herbelin authored
    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
  5. Improving error message when abtraction over goal (abstract_list_all

    herbelin authored
    used when applying schemes - induction, rewrite, ...) is well-typed
    but not of the right type.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15853 85f007b7-540e-0410-9357-904b9bb8a0f7
  6. En cours pour 'generalize in clause' et 'induction in clause'

    herbelin authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15852 85f007b7-540e-0410-9357-904b9bb8a0f7
  7. En cours pour bug 2836

    herbelin authored
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15851 85f007b7-540e-0410-9357-904b9bb8a0f7
  8. Makefile.build: easier compilation with timings info

    letouzey authored
     On a reasonable platform equipped with a /usr/bin/time, a simple
     "make TIMED=1" should provide you with timings of the .v compilations.
    
     If you don't have /usr/bin/time, or prefer a different output format,
     you can still do a "make TIMECMD='...'".
    
     For storing the timings in a spreadsheet, simply do:
     "make TIMED=1 2> timings.csv"
     and then import this csv in your favorite office program,
     with whitespace as separator.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15850 85f007b7-540e-0410-9357-904b9bb8a0f7
  9. @ppedrot

    Getting rid of Compat in the checker.

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

    Adding a nominal typing layer to Metasyntax in order to clarify

    ppedrot authored
    things up. Records are used instead of their equivalents as tuples.
    This is maybe syntactically heavier, but this is semantically
    equivalent and easier to understand.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15848 85f007b7-540e-0410-9357-904b9bb8a0f7
  11. @ppedrot

    Moved Compat to parsing. This permits to break the dependency of the

    ppedrot authored
    kernel on CAMLP4/5 structures, and consequently should also erase
    such structures from vo files.
    
    This modification requires some code duplication, mainly while
    reimplementing our own location data type. This is chiefly visible
    in the ml4 files, where CAMLP4/5 locations must be manually converted
    to our locations with an explicit (!@) cast operator.
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7
Something went wrong with that request. Please try again.