aboutsummaryrefslogtreecommitdiff
path: root/toplevel/command.mli
AgeCommit message (Expand)Author
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
2016-09-29Fix bug #4869, allow Prop, Set, and level names in constraints.Matthieu Sozeau
2016-06-18Reuse the typing_flags datatype for inductives.Pierre-Marie Pédrot
2016-06-18Moving the typing_flags to the environment.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-14Assume totality: dedicated type rather than boolArnaud Spiwack
2016-01-20Update copyright headers.Maxime Dénès
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-28Univs: fix bug #4375, accept universe binders on (co)-fixpointsMatthieu Sozeau
2015-10-27Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesMatthieu Sozeau
2015-10-08Axioms now support the universe binding syntax.Pierre-Marie Pédrot
2015-09-25Propagate `Guarded` flag from syntax to kernel.Arnaud Spiwack
2015-09-25Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...Arnaud Spiwack
2015-09-14Univs: Add universe binding lists to definitionsMatthieu Sozeau
2015-06-24Add corresponding field in `VernacInductive`.Arnaud Spiwack
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-21Add the possibility of defining opaque terms with program.mlasson
2015-01-12Update headers.Maxime Dénès
2015-01-05kernel/ind Change interface of declare_mind and declare_mutualMatthieu Sozeau
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-07-01Add toplevel commands to declare global universes and constraints.Matthieu Sozeau
2014-06-18Proofs now take and return an evar_universe_context, simplifying interfacesMatthieu Sozeau
2014-06-08Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofPierre-Marie Pédrot
2014-05-06Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Yves Bertot
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-08-08get rid of closures in global/proof stategareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-05-12Use the Hook module here and there.ppedrot
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-05-08Declaration of multiple hypotheses or parameters now share typingherbelin
2013-03-22Fix bug# 2994, 2971 about better error messages.msozeau
2013-03-13Modules and ppvernac, sequel of Enrico's commit 16261letouzey
2013-03-11Allowing (Co)Fixpoint to be defined local and Let-style.ppedrot
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of identifierppedrot
2012-08-24Assumption commands are now displayed as unsafe in Coqide.aspiwack
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...msozeau
2012-03-14Integrated obligations/eterm and program well-founded fixpoint building to to...msozeau
2012-03-02Noise for nothingpboutill
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-02-11Annotations at functor applications:letouzey
2011-02-10More comments and less doublons in some mlipboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:03:18 +0000