aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-04-17Matching patterns: fixed allow_partial_app which was not working onherbelin
2013-04-17Fix of r16257 in r16205 for "errors raised by check_evar_instance wereherbelin
2013-04-17Coqmktop: dynlink is now mandatory due to Maxime's native-compilerletouzey
2013-04-17Coqc: repair localisation of errors in filesletouzey
2013-04-17Using Parameter instead of Variable in test-suite/outputherbelin
2013-04-17Improving error message in explain_cannot_find_well_typed_abstraction:herbelin
2013-04-17Like in r16346, do not filter local definitions (here in theherbelin
2013-04-17Added group properties of eq_refl, eq_sym, eq_transherbelin
2013-04-16Fixing #2968. This is quite brittle though, because we are messingppedrot
2013-04-16Added regression test for bug #3023 which was solved by Matthieu'sherbelin
2013-04-16More in IArrayppedrot
2013-04-15Minor simplifications in Declaremods and Safe_typingletouzey
2013-04-15Declaremods: drop some useless stuff (slight gain in vo size)letouzey
2013-04-15Checker: vo validation checks the absence of Var/Evar/Metaletouzey
2013-04-15Checker : a md5-based way to ensure checker/values.ml is always in syncletouzey
2013-04-15votour: a small tool for guided tours of .voletouzey
2013-04-15Checker: vo validation is now done in check.ml (and always)letouzey
2013-04-15Checker: get rid of code handling section variablesletouzey
2013-04-15Checker: empty sections hardcoded in cb and mindletouzey
2013-04-15Checker: reified encoding of .vo types in values.mlletouzey
2013-04-15Checker: regroup all vo-related types in cic.mliletouzey
2013-04-15anew_instance should not consume the locality twicegareuselesinge
2013-04-15More functional implementation of locality_flag and program_modegareuselesinge
2013-04-11Backport r16394 from 8.4:msozeau
2013-04-10Equality: avoid some unprotected List.nth (fix #2837)letouzey
2013-04-09Added a module of immutable arrays. Not as full as CArray, but shouldppedrot
2013-04-08Enrich test-suite with a test for #3022.ppedrot
2013-04-05Allow catching of WrongAbstractionType, fixing a regression from 8.4msozeau
2013-04-04Small doc fix : module subtyping cannot force access of opaquesletouzey
2013-04-03Removing two Pervasives.compare from Term.ppedrot
2013-04-03Fix for bug #3017: wrong handling of the unresolvability statusmsozeau
2013-04-02Revised infrastructure for lazy loading of opaque proofsletouzey
2013-04-02Mod_subst.force: avoid using join when only one substletouzey
2013-04-02Minor cleanup concerning Mod_subst.MBImapletouzey
2013-04-02Exporting the SearchAbout filter.ppedrot
2013-03-30Continuation of r16346 on filtering local definitions. Refinedherbelin
2013-03-28Safe_typing+Libary: use some arrays instead of lists in vo structuresletouzey
2013-03-28Safe_library : a record type for compiled_library instead of large tupleletouzey
2013-03-26Synchronizing loadpath with the backtrack mechanism.ppedrot
2013-03-26Moved the Loadpath part of Library to its own file, and documentedppedrot
2013-03-25Typo in refman (fix #2962)letouzey
2013-03-25Enrich test-suite with a test for #2928letouzey
2013-03-25Enrich test-suite with a test for #2734letouzey
2013-03-25Native compiler: hash-consing of generated code and values.mdenes
2013-03-25Add the test-case of bug 2750 in the test-suiteletouzey
2013-03-25Native compiler: timing info for reification in debug mode.mdenes
2013-03-25Native compiler: Inlined constants are now compiled, fixing a bug reported bymdenes
2013-03-25Normalized type for Vector.map2pboutill
2013-03-25Fix bug #2989: make unification.ml able to deal with canonical structure in a...pboutill
2013-03-25cbn can be called by Evalpboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 23:33:40 +0000