aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-01-25Fix compilation with camlp5 (Closes: #2487)glondu
2011-01-25Update .gitignoreglondu
2011-01-25Add a test for sorting all universes of stdlibglondu
2011-01-25Rewrite sort_universes to minimize the number of universesglondu
2011-01-20Numbers: simplier spec for testbitletouzey
2011-01-12Fix formatting issue in refmanglondu
2011-01-11Fix ocamlbuild-based build systemglondu
2011-01-11Remove references to -ide option of coqmktopglondu
2011-01-11In univ.ml, put universe_level primitives in its their own sub-moduleglondu
2011-01-11Add [Typeclasses Debug] option that respects backtracking, solvemsozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 09:56:01 +0000