aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Expand)Author
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-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
2019-04-05Merge PR #9685: [vernac] Small cleanup to remove assert false.Vincent Laporte
2019-04-03Protect some I/O routines from SIGALRMMaxime Dénès
2019-03-30[vernac] Small cleanup to remove assert false.Emilio Jesus Gallego Arias
2019-03-27[vernac] [stm] Tweak `with_fail` and hopefully fix the semantics.Emilio Jesus Gallego Arias
2019-03-27[vernac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-25[Vernacular] Deprecate the “Show Script” commandVincent Laporte
2019-03-04[stm] unfocus when edition exits the proof (fix #9431)Enrico Tassi
2019-02-22[library] Remove `-boot` option.Emilio Jesus Gallego Arias
2019-02-08Merge PR #9525: Remove global output_native_objects flag.Emilio Jesus Gallego Arias
2019-02-08Merge PR #9523: Make boot flag into a normal option (no global flag).Emilio Jesus Gallego Arias
2019-02-08Merge PR #9481: [parsing] Use AST node for main parsing entry.Enrico Tassi
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
2019-02-08Make boot flag into a normal option (no global flag).Gaëtan Gilbert
2019-02-08[stm] Filter some more arguments that shouldn't be sent to workers.Emilio Jesus Gallego Arias
2019-02-05[parsing] Use AST node for main parsing entry.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:36:59 +0000