aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2010-02-26Coqc: on win32, let's call coqtop.exe by default, not coqtop.opt.exeletouzey
2010-02-26Correction du bug #2214 + maj liens webnotin
2010-02-25mingw32 cross-compilation: coqide.exe as a GUI program, nicer ./build scriptletouzey
2010-02-25ide/coq_lex.ml in .gitignoreletouzey
2010-02-25Enabled natdynlink hack on Mac OS 10.6thutchin
2010-02-25In the git-specific part of Makefile.build, call to hostname gave optionthutchin
2010-02-25Various fixes in interp, session switching and backtrackingvgross
2010-02-25Changes in lexing and tagging.vgross
2010-02-25Ignoring .spit/.spot files from OCamlSpotterthutchin
2010-02-24Win32 cross-compilation from debian: build of coqide.exe and other binariesletouzey
2010-02-24correction of bug #2088jforest
2010-02-22Improve unification when evars and metas are mixed.msozeau
2010-02-19added validation of delta_resolver (which seem to have an impact on typing)barras
2010-02-19[checker] fixed vo validation problems, module incompatibilities remainbarras
2010-02-19Fixing compilation issuesvgross
2010-02-18Removed redundant and ill-named technical lemma.gmelquio
2010-02-18Removed SeqProp's dependency on Classical.gmelquio
2010-02-18Removed Rtrigo's dependency on Classical.gmelquio
2010-02-18Fixing modules names.vgross
2010-02-18Experimental build of coqtop.exe + plugins via cross-compilation linux-->win32letouzey
2010-02-18Adding uim filesvgross