aboutsummaryrefslogtreecommitdiff
path: root/vernac/comAssumption.ml
AgeCommit message (Expand)Author
2019-11-29Remove deprecated Typeclasses Axioms Are Instances.Théo Zimmermann
2019-10-28Merge PR #10950: [declare] Split universe and inductive declaration code to v...Gaëtan Gilbert
2019-10-25[declare] Generalize kind type on declareDefEmilio Jesus Gallego Arias
2019-10-24[declare] Split universe declaration code to vernac/Emilio Jesus Gallego Arias
2019-10-14Use kernel info from Global for Lib.sections_{depth,are_opened}Gaëtan Gilbert
2019-10-13Fix #10888: Context import behaviour in modtypeGaëtan Gilbert
2019-10-05Fix #10669 incorrect substitution in context outside sectionGaëtan Gilbert
2019-10-05Cleanup ComAssumptionGaëtan Gilbert
2019-10-05Move do_primitive from comassumption to its own module.Gaëtan Gilbert
2019-10-05Declare universes for variables outside of Declare.declare_variableGaëtan Gilbert
2019-08-19[declare] Use `binding_kind` for implicit kind instead of boolean.Emilio Jesus Gallego Arias
2019-08-08Emit Feedback.AddedAxiom in Declare instead of higher layersGaëtan Gilbert
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-03declare_variable: path is always Lib.cwd()Gaëtan Gilbert
2019-07-03Declare section variables in direct style "without" an objectGaëtan Gilbert
2019-07-01[declare] Separate kinds from entries in constant declarationEmilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-06-25Remove the internal_flag argument from Declare API.Pierre-Marie Pédrot
2019-06-24Use named records instead of tuples where `polymorphic` used to be.Gaëtan Gilbert
2019-06-24[api] Remove `polymorphic` type alias, use labels instead.Emilio Jesus Gallego Arias
2019-06-24[api] Move `locality` from `library` to `vernac`.Emilio Jesus Gallego Arias
2019-06-24[lemmas] [proof] Split proof kinds into per-layer components.Emilio Jesus Gallego Arias
2019-06-24Duplicate the type of constant entries in Proof_global.Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-16Turning "manual_implicits" into a list of position in impargs.ml.Hugo Herbelin
2019-06-16Adding location in warning telling implicit arguments differ in term and type.Hugo Herbelin
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-06-08Adding a new kind of assumption to track assumption coming from "Context".Hugo Herbelin
2019-05-23Fixing typos - Part 3JPR
2019-05-21Remove definition-not-visible warningGaëtan Gilbert
2019-05-20[Classes] Use prepare_parameter from DeclareDef.Emilio Jesus Gallego Arias
2019-04-10Functionalize env in type classesMaxime Dénès
2019-03-27[vernac] Thread proof state to declare_assumption for warningEmilio Jesus Gallego Arias
2019-03-27[vernac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-22Apply implicit binders to Hypothesis inside sections.Jasper Hugunin
2019-02-20Merge PR #9529: Change Primitive message: "is registered" -> "is declared".Vincent Laporte
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-08Change Primitive message: "is registered" -> "is declared".Gaëtan Gilbert
2019-02-05Make Program a regular attributeMaxime Dénès
2019-02-04Primitive integersMaxime Dénès
2018-11-27Merge PR #9046: Goptions.declare_* functions return unit instead of a write_f...Emilio Jesus Gallego Arias
2018-11-24Merge PR #8933: Make initial evar map argument to check_evars_are_solved opti...Pierre-Marie Pédrot
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-22Deprecate Typeclasses Axioms Are InstancesGaëtan Gilbert
2018-11-21Make initial evar map argument to check_evars_are_solved optional.Gaëtan Gilbert
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-10-16{Univops -> Vars}.universes_of_constrGaëtan Gilbert
2018-10-16UnivGen.constr_of_glob_univ -> Constr.mkRefGaëtan Gilbert
2018-10-05Using smart mkLambdaCN/mkProdCN.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 12:22:17 +0000