aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* test-suite/Makefile: add a rule to build all_stdlib.v (for the bench)Gravatar glondu2011-01-27
* Make simpl use the proper constant when folding (mutual) fixpointsGravatar letouzey2011-01-27
* Fix compilation with camlp5 (Closes: #2487)Gravatar glondu2011-01-25
* Update .gitignoreGravatar glondu2011-01-25
* Add a test for sorting all universes of stdlibGravatar glondu2011-01-25
* Rewrite sort_universes to minimize the number of universesGravatar glondu2011-01-25
* Numbers: simplier spec for testbitGravatar letouzey2011-01-20
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 12:18:52 +0000