aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-04-23Egramcoq+Lexer : no need for an init_functionletouzey
2013-04-23Indfun : use States.with_state_protection instead of freeze/unfreezeletouzey
2013-04-23Egramcoq: clean an ugly code snippetletouzey
2013-04-23minor cleanup in coqtop.mlletouzey
2013-04-23coqtop -compile: avoid with_heavy_rollback when non-interactiveletouzey
2013-04-23Coqtop -compile : avoid saving init state when compiling just one fileletouzey
2013-04-23Remove deprecated option -no-hash-consing (currently doing nothing)letouzey
2013-04-22code simplifications concerning Summaryletouzey
2013-04-22Declaremods: some more minor cleanupletouzey
2013-04-19Fix compilation of fake_idegareuselesinge
2013-04-19interface.mli and serialize.ml reworked to avoid copy/paste of typesgareuselesinge
2013-04-18coqc and coqmktop migrated in tools/, get rid of scripts/ subdirletouzey
2013-04-18Coqdep: add an -exclude-dir option (wish mentionned in #3025)letouzey
2013-04-18Coqc: accept -exclude-dir + some others + cleanup (fix #3025)letouzey
2013-04-18Finer fix for bug 3017, mark unresolvability only of goals that aremsozeau
2013-04-18Only arguments declared as implicit can be renamedgareuselesinge
2013-04-18Fix #3001 (rename arg of global cst inside section)gareuselesinge
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 12:39:25 +0000