aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2010-03-23Fix bug in backtracking.vgross
2010-03-23debuggingvgross
2010-03-19Removing unexpected printing of debug output (see bug report #2271).herbelin
2010-03-19Définition de GRAMMARCMA: parsing/grammar.cma n'était plus installé, ce qu...notin
2010-03-18kills a warning about vo in checker/safe_typingletouzey
2010-03-18Makefile.build: (slightly) more robust sed invocation for parsing camlp4deps/...letouzey
2010-03-18Myocamlbuild: slight simplification of code for .ml4letouzey
2010-03-15Oops, don't use zeta by default.msozeau
2010-03-15Stop dropping evar constraints when building a new goal evar defs.msozeau
2010-03-15Fix splitting evars tactics and stop dropping evar constraints whenmsozeau
2010-03-12fixed minor pbs with test casesbarras
2010-03-12fixed confusion between number of cstr arguments and number of pattern variab...barras
2010-03-11introduced lazy computation of size info in the guard conditionbarras
2010-03-11Update manual on search commandspuech
2010-03-11Minimal test suite for search commandspuech
2010-03-11fix [Search] when the result has no hypothesis & constant comparisonpuech
2010-03-11No delta-reduction in libtypes anymorepuech
2010-03-11Filter out "_subproof" objects from search resultspuech
2010-03-10NMake: remove useless tactics abstract_pair, nicer commentsletouzey
2010-03-10NMake: Reorganization, interface for NMake_gen, explicit View, tactic destr_t...letouzey
2010-03-10NMake_gen.ml: robustness w.r.t size, remove old commented stuff about shiftlletouzey
2010-03-08Consider OccurCheck a catchable exception.msozeau
2010-03-08Application des patches envoyés par F. Besson pour micromeganotin
2010-03-07Reorder resolution of type class and unification constraints.msozeau
2010-03-07Fix lifting of constraints in generalized rewriting tactic.msozeau
2010-03-07Fix treatment of remaining unification constraints: raise a moremsozeau
2010-03-06Fixes in rewrite and a Elimination/Case to Scheme:msozeau
2010-03-06Adding Function as keyword for coqdocthery
2010-03-05Makefile: some more cleanupletouzey
2010-03-05Minor fixes.msozeau
2010-03-05Improvements in generalized rewriting:msozeau
2010-03-05Fix [autounfold] to accept general [in] clauses.msozeau
2010-03-05Add a generic tactic option builder. Use it in firstorder to set themsozeau
2010-03-04Makefile: a nicer hack concerning ocamlopt with no .mli: -intf-suffix .cmi (t...letouzey
2010-03-04Makefile: cleanup of comments + a few words about recent changes in dev/doc/b...letouzey
2010-03-04Makefile: no more separate stagesletouzey
2010-03-04Coqdep_boot: when emultating ocamldep, avoid outputting empty answerletouzey
2010-03-04Makefile: try to avoid rare make failures related with make -j + ocamlopt + .cmiletouzey
2010-03-04Makefile: cleanup of variables containing lists of files, such as MLFILESletouzey
2010-03-04Makefile: make devdocclean was not removing *.dep.ps, btw let's remove *.dep....letouzey
2010-03-04Makefile: factorization of default rules for .cmi/.cmo/.cmxletouzey
2010-03-04Makefile: the .ml of .ml4 are now produced explicitely (in binary ast form)letouzey
2010-03-04Makefile: hide the trick ...||(RV=$$?;rm $@; exit $${RV}) under a macro $(TOT...letouzey
2010-03-01amelioration mineure dans Functionjforest
2010-02-26New backtracking code + fix bug #2082.vgross
2010-02-26Introducing a dual stack setupvgross
2010-02-26New API for backtracking.vgross
2010-02-26Redispatch of printing tweaking hooks.vgross
2010-02-26Some more adaptations for Debian-->mingw32letouzey
2010-02-26Slight reorganisation of make clean, new entry cleankeepvoletouzey