aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Expand)Author
2019-06-17Merge universe quantification and delayed constraints in opaque proofs.Pierre-Marie Pédrot
2019-06-17Allow to delay polymorphic opaque constants.Pierre-Marie Pédrot
2019-06-17[proof] drop parameter from terminator typeEmilio Jesus Gallego Arias
2019-06-17[proof] Unify obligation proof save path: Part I, declareOblEmilio Jesus Gallego Arias
2019-06-17[proofs] Store hooks in the proof object.Emilio Jesus Gallego Arias
2019-06-12Fix #9455: avoid update_global_env when unchanged Global.universes()Gaëtan Gilbert
2019-06-11STM: encode in static types that vernac_when is only used when VtSideffGaëtan Gilbert
2019-06-09[proof] Uniformize Proof_global APIEmilio Jesus Gallego Arias
2019-06-09[save_proof] Make terminator API internal.Emilio Jesus Gallego Arias
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-06Merge PR #10299: Lazy substitution of section contexts in opaque proofsMaxime Dénès
2019-06-04Rename Proof_global.{t -> stack}Gaëtan Gilbert
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-06-04Remove the discharge segment from vo files.Pierre-Marie Pédrot
2019-06-04Slightly tweak the representation of dischargeable opaque proofs.Pierre-Marie Pédrot
2019-06-04Do not substitute opaque constants when discharging.Pierre-Marie Pédrot
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-27Remove the delayed universe table from object files.Pierre-Marie Pédrot
2019-05-24Merge PR #10233: Fixing typos - Part 3Théo Zimmermann
2019-05-24Merge PR #10209: Fix #10208 don't fail when passed extensionless -topfileEnrico Tassi
2019-05-24Remove the indirect opaque accessor hooks from Opaqueproof.Pierre-Marie Pédrot
2019-05-24Statically ensure the content of delayed proofs in vio file.Pierre-Marie Pédrot
2019-05-24Remove a useless call to the Future API for opaque proofs in the STM.Pierre-Marie Pédrot
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-22Fix ambiguous comment problemTalia Ringer
2019-05-22unified style for new hooks and old hooksTalia Ringer
2019-05-22Merge remote-tracking branch 'origin/master' into stm+doc_hookTalia Ringer
2019-05-22Fix #10208 don't fail when passed extensionless -topfileGaëtan Gilbert
2019-05-21[loadpath] Make loadpath handling self-contained and move to vernacEmilio Jesus Gallego Arias
2019-05-21Merge PR #10160: Miscellaneous fixes related to the command lineVincent Laporte
2019-05-21Remove undocumented Instance : ! syntaxGaëtan Gilbert
2019-05-20Remove VtUnknown classificationMaxime Dénès
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-14Removing no more existing option -emacs-U.Hugo Herbelin
2019-05-14Ensuring suffix of file to compile also for -vio2vo checking.Hugo Herbelin
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-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-29[stm] Add hooks for document actions.Emilio Jesus Gallego Arias
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-17Merge PR #9876: Command-line setters for optionsEmilio Jesus Gallego Arias
2019-04-16Command-line setters for optionsGaëtan Gilbert
2019-04-12Unify Set and Unset handling for optionsGaëtan Gilbert
2019-04-11[stm] Report correct ids on some errors where it was dummy.Shachar Itzhaky
2019-04-09[api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:58:22 +0000