aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2019-06-04[rewrite] Add Morphism syntax made different for module type parametersEnrico Tassi
2019-06-04[function] always open a proof when used with `wf` or `measure`Enrico Tassi
2019-06-04Rename Proof_global.{pstate -> t}Gaëtan Gilbert
2019-06-04Funind: use maybe_open_proof a bit lessGaëtan Gilbert
2019-06-04Alternate syntax for ![]: VERNAC EXTEND Foo STATE proofGaëtan Gilbert
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-06-04rewrite.ml: remove outdated commentGaëtan Gilbert
2019-06-04rewrite.ml: drop the id returned by new_instance earlierGaëtan Gilbert
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-27Ensure dynamically that opaque definitions come with their type.Pierre-Marie Pédrot
2019-05-27Merge PR #10237: Fix some incorrect uses of proof-local environmentPierre-Marie Pédrot
2019-05-25Documenting syntax "injection ... as [= pat1 ... patn ]".Hugo Herbelin
2019-05-24Merge PR #10233: Fixing typos - Part 3Théo Zimmermann
2019-05-24Use global env in numeral and string notationsMaxime Dénès
2019-05-24Stop using pstate in global print queriesGaëtan Gilbert
2019-05-24Remove the indirect opaque accessor hooks from Opaqueproof.Pierre-Marie Pédrot
2019-05-23Fixing typos - Part 3JPR
2019-05-23Merge PR #10221: Fixing typos - Part 2 (reopening of #10218)Théo Zimmermann
2019-05-23Merge PR #10185: Remove undocumented Instance : ! syntaxVincent Laporte
2019-05-23Fixing typos - Part 2JPR
2019-05-22Partly revert micromega parsing using typeclasses.Frédéric Besson
2019-05-21Remove definition-not-visible warningGaëtan Gilbert
2019-05-21Remove undocumented Instance : ! syntaxGaëtan Gilbert
2019-05-21Merge PR #10174: Further cleanup of the side-effect machineryGaëtan Gilbert
2019-05-20Remove VtUnknown classificationMaxime Dénès
2019-05-20Remove Refine Instance Mode optionMaxime Dénès
2019-05-19Parameterize the constant_body type by opaque subproofs.Pierre-Marie Pédrot
2019-05-14Merge PR #8893: Moving evars_of_term from constr to econstrPierre-Marie Pédrot
2019-05-14Allow run_tactic to return a value, remove hack from ltac2Gaëtan Gilbert
2019-05-13Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.Hugo Herbelin
2019-05-13Moving Evd.evars_of_term from constr to econstr + consequences.Hugo Herbelin
2019-05-13Merge PR #9887: [api] Remove 8.10 deprecations.Gaëtan Gilbert
2019-05-11Merge PR #10052: Cleanup the hypothesis conversion functionHugo Herbelin
2019-05-10Split the hypothesis conversion check in a conversion + ordering check.Pierre-Marie Pédrot
2019-05-10Make the check flag of conversion functions mandatory.Pierre-Marie Pédrot
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-05-07Improve field_simplify on fractions with constant denominatorthery
2019-05-04Merge PR #9926: [vernac] [ast] Make location info an attribute of vernaculars.Pierre-Marie Pédrot
2019-05-03Fix #10054: Numeral Notations without the ltac plugin.Pierre-Marie Pédrot
2019-05-02Merge PR #10017: Exposing a change_no_check tacticPierre-Marie Pédrot
2019-04-30Deprecating convert_concl_no_check.Hugo Herbelin
2019-04-30fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType` interfaceGeorges Gonthier
2019-04-29Exposing a change_no_check tactic.Hugo Herbelin
2019-04-29Merge PR #9983: Hypothesis conversion allocates a single evarHugo Herbelin
2019-04-29Merge PR #9651: [ssr] Add tactics under and overCyril Cohen
2019-04-29[meta] [dune] Fix discrepancies in plugin namesEmilio Jesus Gallego Arias
2019-04-25[vernac] [ast] Make location info an attribute of vernaculars.Emilio Jesus Gallego Arias
2019-04-25Add a typing colon in the output of the Search ssreflect vernacularErik Martin-Dorel
2019-04-23Deprecate the *_no_check variants of conversion tactics.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:22:51 +0000