aboutsummaryrefslogtreecommitdiff
path: root/ide/coq.ml
AgeCommit message (Expand)Author
2010-02-26New backtracking code + fix bug #2082.vgross
2010-02-26Introducing a dual stack setupvgross
2010-02-26New API for backtracking.vgross
2010-02-26Redispatch of printing tweaking hooks.vgross
2010-02-12Simplify backtrackingvgross
2010-02-12Delineating a API for Coq inside toplevel/vernac.mlvgross
2010-02-12Refactoring of the printing optionsvgross
2010-01-28New command Declare Reduction <id> := <conv_expr>.letouzey
2010-01-11Revert "Isolation of proof-displaying code"vgross
2010-01-11Isolation of proof-displaying codevgross
2009-12-11Deport the backtracking code out of the idevgross
2009-12-08Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...letouzey
2009-12-03Fix bug #2191 : Serious "undo" performance degradation since 8.2pl1vgross
2009-11-19Refactoring of coqide backtrack code, with the intent to put everythingvgross
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-10-27Add a new vernacular command for controling implicit generalization ofmsozeau
2009-10-04Removal of trailing spaces.serpyc
2009-09-29kills the old backtracking framework and replaces it withvgross
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-14Ajout de la gestion de Local et Global pour les options (au sens deaspiwack
2009-08-03Added "etransitivity".herbelin
2009-08-02Improved parameterization of Coq:herbelin
2009-06-22remove some unused functions (which are part of a soon-to-be obsoletevgross
2009-06-11Simplifying the call to print_no_goals and not calling it when no goalherbelin
2009-06-07Partial simplification of undo mechanism, relying only on Courtieu'sherbelin
2009-05-27dead code pruningvgross
2009-05-13minor bugfixes. CoqIde development will resume soon now ...vgross
2009-03-07- per session coq command stackvgross
2009-03-06fixed groebner as a plugin + pattern matching Timeoutbarras
2009-03-04Temporary hack to make coqide.byte work (backport r11948) (see #2062)glondu
2009-02-11Report des revisions #11826, #11828 et #11829 de v8.2 vers trunknotin
2009-01-17DISCLAIMERpuech
2009-01-06Conversion du fichier 'revision' en un fichier .ml + correction d'un bug dans...notin
2008-12-19Nettoyage des variables Coq et amélioration de coqmktop. Lesnotin
2008-12-14Generalized binding syntax overhaul: only two new binders: `() and `{},msozeau
2008-11-09More factorization of inductive/record and typeclasses: move classmsozeau
2008-10-28Native "Declare ML Module" when possibleglondu
2008-10-03Minor fixes related to coqdoc and --interpolate and the dependentmsozeau
2008-07-18- Rebranchement backtrack du langage déclaratif dans Coqideherbelin
2008-07-10Bug résiduel du backtrack de coqide se produisant lorsque la limite deherbelin
2008-07-01Encore une suite au 11188/11193 (c'était pas un bon jour)herbelin
2008-06-13CoqIDE: 2 problèmes de undo encore:herbelin
2008-06-11Plutôt que de reposer sur le vernacexpr pour détecter les débuts deherbelin
2008-06-09On prend des risques en tentant d'optimiser encore plus le undo en casherbelin
2008-06-06- On adopte finalement la méthode de Pierre Courtieu pour le undo deherbelin
2008-05-30- Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"herbelin
2008-05-28Réorganisation fenêtre d'accueil CoqIDE et About; nouvelle image deherbelin
2008-05-26Réorganisation des points d'appui du undo de CoqIDE (type reset_info).herbelin
2008-05-26Bug undo CoqIDE sur Endherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:36:57 +0000