aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fix formatting issue in refmanGravatar glondu2011-01-12
* Fix ocamlbuild-based build systemGravatar glondu2011-01-11
* Remove references to -ide option of coqmktopGravatar glondu2011-01-11
* In univ.ml, put universe_level primitives in its their own sub-moduleGravatar glondu2011-01-11
* Add [Typeclasses Debug] option that respects backtracking, solveGravatar msozeau2011-01-11
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
* Use dashed lines for equivalence edges in dot output of universesGravatar glondu2011-01-11
* More coherent comment orderingGravatar glondu2011-01-11
* Fix some typosGravatar glondu2011-01-11
* ratrapage exception, deja fait ...Gravatar bgregoir2011-01-11
* Fixing an uncaught exception bug with use of vmcastGravatar herbelin2011-01-07
* MacOS integrationGravatar pboutill2011-01-07
* Separate load_file handler in coqideGravatar pboutill2011-01-07
* Coqide is not built with coqmktop any moreGravatar pboutill2011-01-07
* Don't install both coqide.byte and coqide.optGravatar pboutill2011-01-07
* Call coqtop with -nois when probing for filesGravatar pboutill2011-01-07
* Fix print in coqideGravatar pboutill2011-01-07
* mli comments for docGravatar pboutill2011-01-07
* Update CHANGESGravatar pboutill2011-01-07
* Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)Gravatar letouzey2011-01-07
* Remove fake alpha-specific case in configureGravatar glondu2011-01-06
* s/appartness/membership/g (Closes: #2470)Gravatar glondu2011-01-06
* Reverted r13715 "Add improved indenters that rely on the current proof state ...Gravatar gmelquio2011-01-06
* Remove Safe_marshalGravatar glondu2011-01-06
* Ndigits: a Pshiftl_nat used in BigN (was double_digits there)Gravatar letouzey2011-01-04
* f_equiv : a clone of f_equal that handles setoid equivalencesGravatar letouzey2011-01-04
* Numbers: some improvements in proofsGravatar letouzey2011-01-03
* Rename the "raw" argument extension into "glob"Gravatar glondu2010-12-27
* ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPEDGravatar glondu2010-12-25
* Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commandsGravatar glondu2010-12-25
* Rename mkR* smart constructors (mostly in funind)Gravatar glondu2010-12-25
* s/raw/glob/g in decl_interp.ml for more consistencyGravatar glondu2010-12-24
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename files in funind to respect new conventionsGravatar glondu2010-12-24
* Remove obsolete script univdot, update dev doc about universesGravatar glondu2010-12-24
* tactics/eqdecide.ml4: avoid a useless argument in decideEqualityGravatar glondu2010-12-24
* Precision in documentation of "decide equality"Gravatar glondu2010-12-24
* Remove the two-argument variant of "decide equality"Gravatar glondu2010-12-23
* Fix diagram in genarg.mliGravatar glondu2010-12-23
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Prepare change of nomenclature rawconstr -> glob_constrGravatar glondu2010-12-23
* More precise documentation for instantiateGravatar glondu2010-12-23
* Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)Gravatar letouzey2010-12-21
* Fixing bug #2454: inversion predicate strategy for inferring the typeGravatar herbelin2010-12-19
* Univ: try to avoid a few lookup in the universe graphGravatar letouzey2010-12-18
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
* Revert last commit 13723 on Univ : minor gains and more complex codeGravatar letouzey2010-12-18
* Univ: an attempt to lazily compact chains of Equiv in a functionnal wayGravatar letouzey2010-12-17
* NPeano.modulo : another trick a la "minus" for having a decreasing argGravatar letouzey2010-12-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-14 04:01:34 +0000