aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
Commit message (Collapse)AuthorAge
* Changement de ide/proofs.ml en ide/ideproofs.ml pour éviter un conflitGravatar aspiwack2010-04-05
| | | | | | | avec le futur commit de la nouvelle machinerie de preuve. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12901 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changing types to reflect futur separation between toplevel and ide.Gravatar vgross2010-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12880 85f007b7-540e-0410-9357-904b9bb8a0f7
* Goal generation deported into ide/coq.ml, single function to obtainGravatar vgross2010-03-23
| | | | | | all current goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12878 85f007b7-540e-0410-9357-904b9bb8a0f7
* New functions for goals fetching.Gravatar vgross2010-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in backtracking.Gravatar vgross2010-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12876 85f007b7-540e-0410-9357-904b9bb8a0f7
* debuggingGravatar vgross2010-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12875 85f007b7-540e-0410-9357-904b9bb8a0f7
* New backtracking code + fix bug #2082.Gravatar vgross2010-02-26
| | | | | | Previous code checkings were too lax, and information was lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12823 85f007b7-540e-0410-9357-904b9bb8a0f7
* Introducing a dual stack setupGravatar vgross2010-02-26
| | | | | | | The first stack lives in coqide and tracks the tagging and locking, the second lives in coq and tracks the commands. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12822 85f007b7-540e-0410-9357-904b9bb8a0f7
* New API for backtracking.Gravatar vgross2010-02-26
| | | | | | | Aside the command stack, the only parameter is the number of step to go back. Went back and forth without sync losses on tests-suite/ide/undo.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Redispatch of printing tweaking hooks.Gravatar vgross2010-02-26
| | | | | | | We want to tweak the printing options when we want to display the results, not when we are evaluating vernac. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12820 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various fixes in interp, session switching and backtrackingGravatar vgross2010-02-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12809 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changes in lexing and tagging.Gravatar vgross2010-02-25
| | | | | | | | Lexing send back an offset couple delimiting beginning and ending of sentences. This couple is used to apply a tag on the whole sentence. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12808 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing compilation issuesGravatar vgross2010-02-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12798 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing modules names.Gravatar vgross2010-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12794 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding uim filesGravatar vgross2010-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12791 85f007b7-540e-0410-9357-904b9bb8a0f7
* Polishing the setup of CoqIDE Input MethodGravatar vgross2010-02-18
| | | | | | | | autodetection via ./configure, automated installation target "install-im", and no more patching. Plus documentation of the procedure in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12790 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change the customization of modifiers (bug #2210)Gravatar vgross2010-02-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12771 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplify backtrackingGravatar vgross2010-02-12
| | | | | | | As we can now jump right onto a closed segment, there is no need for complicated pattern matching. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delineating a API for Coq inside toplevel/vernac.mlGravatar vgross2010-02-12
| | | | | | | | | | | | | Coq use case are mostly thoses : - parsing a char stream to get a vernac expr - evaluating a vernac expr with backtracking - turning a knob with a vernac expr, no backtracking - loading an entire file - compiling an entire file - backtracking (no clean API for this yet) - peeking Coq state info (no clean API for this yet) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12756 85f007b7-540e-0410-9357-904b9bb8a0f7
* Refactoring of the printing optionsGravatar vgross2010-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12755 85f007b7-540e-0410-9357-904b9bb8a0f7
* New command Declare Reduction <id> := <conv_expr>.Gravatar letouzey2010-01-28
| | | | | | | | Let's avoid writing huge "Eval ... in ..." lines :-) Will be used in particular soon in NMake for defining function via Definition ... := Eval ... in ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12699 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix uncaught exceptionGravatar vgross2010-01-14
| | | | | | | On windows platform, exceptions are not always encoded in utf-8, thus failing the assert. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12675 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "Isolation of proof-displaying code"Gravatar vgross2010-01-11
| | | | | | | This reverts commit 8162ee31152eb2f99af724e88a7e15a899c17811. Not the smartest thing to do on the verge of tagging. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12649 85f007b7-540e-0410-9357-904b9bb8a0f7
* Isolation of proof-displaying codeGravatar vgross2010-01-11
| | | | | | | | | | The formatting logic is now isolated in ide/proofBrowser.ml, and the goal printing logic is deported inside ide/coq.ml. Also, the proof mode special printing has been cut out. Finally, turn every call to show_goals_full into show_goals, and use show_goals_full as the body of show_goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12648 85f007b7-540e-0410-9357-904b9bb8a0f7
* Patches and instructions to enable Input Method support in CoqIDE.Gravatar vgross2009-12-21
| | | | | | | TODO: don't patch the ELatin IM, create a separate IM or push the patch upstream. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12604 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deport the backtracking code out of the ideGravatar vgross2009-12-11
| | | | | | | Backtracking code now lies entirely into ide/coq.ml. Datatypes have been tweaked to easen the separation to come. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12576 85f007b7-540e-0410-9357-904b9bb8a0f7
* Migration of ProtectedToplevel and Line_oriented_parser into new contrib ↵Gravatar letouzey2009-12-08
| | | | | | | | | Interface the ProtectedLoop feature was used only by CoqInterface. Idem for stuff in Line_oriented_parser git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12573 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2197 (option show_toolbar not taken into account at startup)Gravatar vgross2009-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12568 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the "detach script windows" feature.Gravatar vgross2009-12-07
| | | | | | See bug #2173. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12567 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2191 : Serious "undo" performance degradation since 8.2pl1Gravatar vgross2009-12-03
| | | | | | | | | This reverts commit 12537 This reverts commit 12199 This reverts commit 12198 This reverts commit 12172 (introduced the bug) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12559 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ergonomy and robustness fixGravatar vgross2009-11-23
| | | | | | | | Sentences are locked up to the period, and it's now possible to eval when there is no final whitespace. CoqIde will refuse to evaluate further if there is no whitespace, though. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12539 85f007b7-540e-0410-9357-904b9bb8a0f7
* Refactoring of coqide backtrack code, with the intent to put everythingGravatar vgross2009-11-19
| | | | | | | | into coqtop. Also, some cleaning in ide/gtk_parsing.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12537 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove dubious call to Obj.magic (and dead code, by the way)Gravatar glondu2009-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12522 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove useless call to Obj.magicGravatar glondu2009-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12521 85f007b7-540e-0410-9357-904b9bb8a0f7
* scripting area now grabs focus at startup.Gravatar vgross2009-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12518 85f007b7-540e-0410-9357-904b9bb8a0f7
* new handling for lexical structures.Gravatar vgross2009-11-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Sentence extraction and proof folding is now done with tags. The lexer has been modified to use a callback to "stamp" the lexical constructs that must be distinguished. new funcs in ide/coqide.ml : apply_tag : GText.buffer -> GText.iter -> (int -> int) -> int -> int -> CoqLex.token -> unit remove_tags : GText.buffer -> GText.iter -> GText.iter -> unit tag_slice : GText.buffer -> GText.iter -> GText.iter -> (GText.buffer -> GText.iter -> GText.iter) -> unit get_sentence_bounds : GText.iter -> GText.iter * GText.iter end_tag_present : GText.iter -> bool tag_on_insert : GText.buffer -> unit force_retag : GText.buffer -> unit toggle_proof_visibility : GText.buffer -> GText.iter -> unit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12517 85f007b7-540e-0410-9357-904b9bb8a0f7
* lexing refactoringGravatar vgross2009-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12516 85f007b7-540e-0410-9357-904b9bb8a0f7
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed 'Toplevel' language from extraction documentation, since it is not ↵Gravatar gmelquio2009-11-04
| | | | | | currently supported. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12467 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added Coqide highlighting for extraction vernacular.Gravatar gmelquio2009-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12448 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed 'dest' from keyword highlighting.Gravatar gmelquio2009-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12447 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integrate a few improvements on typeclasses and Program from the equations ↵Gravatar msozeau2009-10-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | branch and remove equations stuff which moves to a separate plugin. Classes: - Ability to define classes post-hoc from constants or inductive types. - Correctly rebuild the hint database associated to local hypotheses when they are changed by a [Hint Extern] in typeclass resolution. Tactics and proofs: - Change [revert] so that it keeps let-ins (but not [generalize]). - Various improvements to the [generalize_eqs] tactic to make it more robust and produce the smallest proof terms possible. Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with [generalize_eqs]. - A few new general purpose tactics in Program.Tactics like [revert_until] - Make transitive closure well-foundedness proofs transparent. - More uniform testing for metas/evars in pretyping/unification.ml (might introduce a few changes in the contribs). Program: - Better sorting of dependencies in obligations. - Ability to start a Program definition from just a type and no obligations, automatically adding an obligation for this type. - In compilation of Program's well-founded definitions, make the functional a separate definition for easier reasoning. - Add a hint database for every Program populated by [Hint Unfold]s for every defined obligation constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
| | | | | | | | | | | | | variables with syntax: [Local?|Global] Generalizable Variable(s)? [all|none|id1 idn]. By default no variable is generalizable, so this patch breaks backward compatibility with files that used implicit generalization (through Instance declarations for example). To get back the old behavior, one just needs to use [Global Generalizable Variables all]. Make coq_makefile more robust using [mkdir -p]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added syntactic coloration for 'Function'.Gravatar gmelquio2009-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12403 85f007b7-540e-0410-9357-904b9bb8a0f7
* note for later : when the tag table is shared, never, ever create twoGravatar vgross2009-10-16
| | | | | | tags with the same name. This fixes file opening. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12396 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "kills the old backtracking framework and replaces it with"Gravatar vgross2009-10-05
| | | | | | This reverts commit 33545cc88bf4b4e19b222afd2d1d264bcba97838. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12373 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removal of trailing spaces.Gravatar serpyc2009-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12371 85f007b7-540e-0410-9357-904b9bb8a0f7
* kills the old backtracking framework and replaces it withGravatar vgross2009-09-29
| | | | | | ProofGeneral-like "Backtrack". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12364 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* removed the double-click / proof hiding association.Gravatar vgross2009-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12328 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 20:53:56 +0000