aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-01-11Add "Print Sorted Universes"glondu
2011-01-11Use dashed lines for equivalence edges in dot output of universesglondu
2011-01-11More coherent comment orderingglondu
2011-01-11Fix some typosglondu
2011-01-11ratrapage exception, deja fait ...bgregoir
2011-01-07Fixing an uncaught exception bug with use of vmcastherbelin
2011-01-07MacOS integrationpboutill
2011-01-07Separate load_file handler in coqidepboutill
2011-01-07Coqide is not built with coqmktop any morepboutill
2011-01-07Don't install both coqide.byte and coqide.optpboutill
2011-01-07Call coqtop with -nois when probing for filespboutill
2011-01-07Fix print in coqidepboutill
2011-01-07mli comments for docpboutill
2011-01-07Update CHANGESpboutill
2011-01-07Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)letouzey
2011-01-06Remove fake alpha-specific case in configureglondu
2011-01-06s/appartness/membership/g (Closes: #2470)glondu
2011-01-06Reverted r13715 "Add improved indenters that rely on the current proof state ...gmelquio
2011-01-06Remove Safe_marshalglondu
2011-01-04Ndigits: a Pshiftl_nat used in BigN (was double_digits there)letouzey
2011-01-04f_equiv : a clone of f_equal that handles setoid equivalencesletouzey
2011-01-03Numbers: some improvements in proofsletouzey
2010-12-27Rename the "raw" argument extension into "glob"glondu
2010-12-25ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPEDglondu
2010-12-25Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commandsglondu
2010-12-25Rename mkR* smart constructors (mostly in funind)glondu
2010-12-24s/raw/glob/g in decl_interp.ml for more consistencyglondu
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-24Rename files in funind to respect new conventionsglondu
2010-12-24Remove obsolete script univdot, update dev doc about universesglondu
2010-12-24tactics/eqdecide.ml4: avoid a useless argument in decideEqualityglondu
2010-12-24Precision in documentation of "decide equality"glondu
2010-12-23Remove the two-argument variant of "decide equality"glondu
2010-12-23Fix diagram in genarg.mliglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-12-23Prepare change of nomenclature rawconstr -> glob_constrglondu
2010-12-23More precise documentation for instantiateglondu
2010-12-21Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)letouzey
2010-12-19Fixing bug #2454: inversion predicate strategy for inferring the typeherbelin
2010-12-18Univ: try to avoid a few lookup in the universe graphletouzey
2010-12-18Univ.constraints made fully abstract instead of being a Set of abstract stuffletouzey
2010-12-18Revert last commit 13723 on Univ : minor gains and more complex codeletouzey
2010-12-17Univ: an attempt to lazily compact chains of Equiv in a functionnal wayletouzey
2010-12-17NPeano.modulo : another trick a la "minus" for having a decreasing argletouzey
2010-12-17Cosmetic : let's take advantage of the n-ary exists notationletouzey
2010-12-17Nicer log2 function for nat (suggested by Hugo)letouzey
2010-12-16Univ: two improvements (speed + space)letouzey
2010-12-15Clenv.connect_clenv without its Evd.foldletouzey
2010-12-15Evar-related speed-up and clarifications in Class_tactics and Rewriteletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 11:19:10 +0000