aboutsummaryrefslogtreecommitdiff
path: root/vernac/comAssumption.ml
AgeCommit message (Expand)Author
2020-11-04Moving interpretation of user-level universes in constrintern.ml.Hugo Herbelin
2020-10-16Fixes/enhancements with local definitions in records.Hugo Herbelin
2020-10-16Generalizing and exporting interp_assumption/interp_definition.Hugo Herbelin
2020-07-02Fix Context with nonmaximplicit.Gaëtan Gilbert
2020-06-26[declare] [api] Removal of duplicated type aliases.Emilio Jesus Gallego Arias
2020-06-26[declare] [api] Removal of deprecated functionsEmilio Jesus Gallego Arias
2020-06-03[declare] Hide internals of variable declaration entries.Emilio Jesus Gallego Arias
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
2020-04-21[declare] [tactics] Move declare to `vernac`Emilio Jesus Gallego Arias
2020-04-15Coqdoc: Exporting location and unique id for binding variables.Hugo Herbelin
2020-03-31Remove special case for implicit inductive parametersMaxime Dénès
2020-03-30[declare] Fuse prepare and declare for the non-interactive path.Emilio Jesus Gallego Arias
2020-03-30[declareDef] More consistent handling of universe bindersEmilio Jesus Gallego Arias
2020-03-30[declare] Make the type of closed entries opaque.Emilio Jesus Gallego Arias
2020-03-19[declare] Bring more consistency to parameters using labelsEmilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-25[vernac] Remove deprecated function.Emilio Jesus Gallego Arias
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
2019-12-16Pretyping.check_evars: make initial evar map optionalGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:59:23 +0000