aboutsummaryrefslogtreecommitdiff
path: root/toplevel/ind_tables.ml
AgeCommit message (Expand)Author
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-01-20Update copyright headers.Maxime Dénès
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-09-23Hopefully better names to constructors of internal_flag, as discussedHugo Herbelin
2015-09-23Give a way to control if the decidable-equality schemes are built likeHugo Herbelin
2015-08-02Reverting 16 last commits, committed mistakenly using the wrong push command.Hugo Herbelin
2015-08-02Give a way to control if the decidable-equality schemes are built likeHugo Herbelin
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-08-30Simplify even further the declaration of primitive projections,Matthieu Sozeau
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-06-17Safer entry point of primitive projections in the kernel, now it does recognizeMatthieu Sozeau
2014-06-08ind_tables: always declare side effects (Closes: HOTT#110)Enrico Tassi
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Rework handling of universes on top of the STM, allowing for delayedMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-08-30ind_tables: properly handling side effectsgareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-05-14Replacing Id.check with Id.is_valid, as its sole use was underppedrot
2013-04-22code simplifications concerning Summaryletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
2012-12-13Using library string functions.ppedrot
2012-11-26Monomorphization (toplevel)ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-08-08Updating headers.herbelin
2012-03-02Noise for nothingpboutill
2011-12-12Proof using ...gareuselesinge
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-10-08Scheme names: Use unprobable names + ensure names do not hide existing namesherbelin
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-02* removed declare_constant and declare_internal_constant vsiles
2010-09-02v13392 port from v8.3 to trunk : correct message when defining inductive schemesvsiles
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-29change the flag "internal" in declare/ind_tables from bool tovsiles
2010-05-29New pass on inductive schemesherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 02:16:41 +0000