aboutsummaryrefslogtreecommitdiff
path: root/vernac/vernacentries.ml
AgeCommit message (Expand)Author
2019-06-04coqpp: add new ![] specifiers for structured proof interactionGaëtan Gilbert
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-28[elaboration] Bidirectionality hintsMaxime Dénès
2019-05-23Fixing typos - Part 3JPR
2019-05-23Merge PR #9895: [loadpath] Make loadpath handling self-contained and move to ...Maxime Dénès
2019-05-23Merge PR #10185: Remove undocumented Instance : ! syntaxVincent Laporte
2019-05-22Merge PR #10173: Fail: don't catch critical errorsEmilio Jesus Gallego Arias
2019-05-21[loadpath] Further cleanup after merge with MlTop.Emilio Jesus Gallego Arias
2019-05-21[loadpath] Make loadpath handling self-contained and move to vernacEmilio Jesus Gallego Arias
2019-05-21Remove definition-not-visible warningGaëtan Gilbert
2019-05-21Remove undocumented Instance : ! syntaxGaëtan Gilbert
2019-05-17Fail: don't catch critical errorsGaëtan Gilbert
2019-05-13Merge PR #10076: [Canonical structures] Annotation to field declarations to p...Enrico Tassi
2019-05-13Merge PR #10061: Print custom grammar entriesVincent Laporte
2019-05-10Use Print Custom Grammar to inspect custom entriesJasper Hugunin
2019-05-10[Canonical structures] “not_canonical” annotation to field declarationsVincent Laporte
2019-05-10Remove various circumvolutions from reduction behaviorsMaxime Dénès
2019-05-07[Record] Une a record to gather field declaration attributesVincent Laporte
2019-05-04Merge PR #9926: [vernac] [ast] Make location info an attribute of vernaculars.Pierre-Marie Pédrot
2019-04-30Remove Global.env from goptions by passing from vernacentriesGaëtan Gilbert
2019-04-29Merge PR #9935: [api] [proof] Alert users that `Vernacstate.Proof_global` is ...Maxime Dénès
2019-04-25[vernac] [ast] Make location info an attribute of vernaculars.Emilio Jesus Gallego Arias
2019-04-12Unify Set and Unset handling for optionsGaëtan Gilbert
2019-04-11Merge PR #9909: Remove all but one call to `Global` in the pretyperPierre-Marie Pédrot
2019-04-10Remove calls to Global.env and Libobject from RecordopsMaxime Dénès
2019-04-10Functionalize env in type classesMaxime Dénès
2019-04-09[api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used.Emilio Jesus Gallego Arias
2019-04-05[api] [proofs] Remove dependency of proofs on interp.Emilio Jesus Gallego Arias
2019-03-30[vernac] Small cleanup to remove assert false.Emilio Jesus Gallego Arias
2019-03-29[parser] initialization based on Loc.t rather than Loc.sourceEnrico Tassi
2019-03-27[vernac] [stm] Tweak `with_fail` and hopefully fix the semantics.Emilio Jesus Gallego Arias
2019-03-27[vernac] Thread proof state to declare_assumption for warningEmilio Jesus Gallego Arias
2019-03-27[vernacular] Make `Show` fail again when no goals remain.Emilio Jesus Gallego Arias
2019-03-27[vernac] Allow path for `save_proof` where no proof state is present.Emilio Jesus Gallego Arias
2019-03-27[vernac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-14Documentation for SPropGaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-12Merge PR #9389: Implement a method for manual declaration of implicits.Emilio Jesus Gallego Arias
2019-03-06Merge PR #9476: Constructor type information uses the expanded form.Gaëtan Gilbert
2019-03-01Move test_mode from Flags to Vernacentries (use point)Gaëtan Gilbert
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
2019-02-23[vernac] Unify declaration hooks.Emilio Jesus Gallego Arias
2019-02-19Make inductive cumulativity flag local to vernacentriesGaëtan Gilbert
2019-02-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
2019-02-08Merge PR #9481: [parsing] Use AST node for main parsing entry.Enrico Tassi
2019-02-05[parsing] Use AST node for main parsing entry.Emilio Jesus Gallego Arias
2019-02-05Make Program a regular attributeMaxime Dénès
2019-02-04Primitive integersMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 01:49:47 +0000