aboutsummaryrefslogtreecommitdiff
path: root/ide/coq_commands.ml
AgeCommit message (Collapse)Author
2020-06-02Move CoqIDE to its own folderMaxime Dénès
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-03[loadpath] Rework and simplify ML loadpath handlingEmilio Jesus Gallego Arias
This PR refactors the handling of ML loadpaths to get it closer to what (as of 2020) the standard OCaml toolchain (ocamlfind, dune) does. This is motivated as I am leaning toward letting the standard OCaml machinery handle OCaml includes; this has several benefits [for example plugins become regular OCaml libs] It will also help in improving dependency handling in plugin dynload. The main change is that "recursive" ML loadpaths are no longer supported, so Coq's `-I` option becomes closer to OCaml's semantics. We still allow `-Q` to extend the OCaml path recursively, but this may become deprecated in the future if we decide to install the ML parts of plugins in the standard OCaml location. Due to this `Loadpath` still hooks into `Mltop`, but other than that `.v` location handling is actually very close to become fully independent of Coq [thus it can be used in other tools such coqdep, the build system, etc...] In terms of vernaculars the changes are: - The `Add Rec ML Path` command has been removed, - The `Add Loadpath "foo".` has been removed. We now require that the form with the explicit prefix `Add Loadpath "foo" as Prefix.` is used. We did modify `fake_ide` as not to add a directory with the empty `Prefix`, which was not used. This exposed some bugs in the implementation of the document model, which relied on having an initial sentence; we have workarounded them just by adding a dummy one in the two relevant cases.
2020-01-17Remove the Tactic menu from CoqIDE.Pierre-Marie Pédrot
Partial fix of #11219: CoqIDE tactics and templates menus are out of sync. Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2018-07-17Remove fourier pluginMaxime Dénès
As stated in the manual, the fourier tactic is subsumed by lra.
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-05-23[vernac] Remove `Save.` command.Emilio Jesus Gallego Arias
It has been deprecated for a while in favor of `Qed`.
2016-01-20Update copyright headers.Maxime Dénès
2015-02-17Remove Whelp commands.Maxime Dénès
Although these commands were never deprecated, they have been unusable for some time now, since they send requests to an Italian server which is no longer alive.
2015-01-12Update headers.Maxime Dénès
2014-09-04Add a [Variant] declaration which allows to write non-recursive variant types.Arnaud Spiwack
Just like the [Record] keyword allows only non-recursive records.
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
I hope I did not forget any place to change. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-23Remove old proof-managment commands Suspend/Resumeletouzey
There're not compatible with the current Backtrack mecanism used both by ProofGeneral and CoqIDE. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15083 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16This adds two option tables 'Printing Record' and 'Printing Constructor'herbelin
that forces a given type to always be printed as a record, or with a constructor, regardless of the setting of 'Printing Records'. And this is that patch that controls printing by type. (patch from Tom Prince) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14286 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Completing support for F5=About by adding About to the state-preserving ↵herbelin
command list git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12225 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-26remove set printing ... and unset printing ... from template menu as they ↵jnarboux
are no useless in coqide git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10994 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-25- Nouvelle option "Set Printing Existential Instances" pour forcerherbelin
l'affichage des instances des evars. - Nouveaux boutons "interrupteurs" pour activer/désactiver à volonté l'affichage des implicites, coercions, notations, etc dans CoqIDE (reste à trouver des icônes appropriées !). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10983 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-16Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9656 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-03whelp + correction bug affichage de coqidecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7102 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17New command "Print Rewrite HindDb dbname".sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03New command "Add Relation ..." (for the new implementation of setoid_*).sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6048 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23"Print Setoids" command added.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5968 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-08added commands to idecorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5870 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-16mise a jour des menusmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5507 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15ajout des Print Scopes dans liste commandes sans effetmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5493 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-04highlightmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5289 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-04search windowcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5288 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-30ameliorations coqidecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5161 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-12plus de syntaxe v8marche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5089 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-09commandes de coqidemarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5081 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-08bug de preferencs/font"marche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5076 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-13CoqIDE: undo immediat sur les commandes ne modifiant pas l'etatfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4145 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-12CoqIde: AccelMap supportmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4001 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-07coqide: toolbar/autosavemonate
Hugo: Suppression du type dans les notations == et <> entre Suppression du type dans les notations == et <> entre volution second traducteur selon discussion TYPES git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3993 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-16oubliletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3932 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-15petit oubliletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3775 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-06coqide: fenetre de cmmandes . undo correctmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3747 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-05IDE: menu templatesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3742 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:48:21 +0000