aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-08-08calling interp by hand is forbiddengareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16686 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Add a (very minimal) Proof General mode to CoqIDEgareuselesinge
documentation available in the help menu git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16685 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08stm: (initial) support for -coq-slavesgareuselesinge
Stm contains many TODO items to improve the thing, but it should be already possible to play with it (but not use it in production). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16684 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08get rid of closures in global/proof stategareuselesinge
In some cases, an 'a -> 'b field is changed into an ('a -> b') option field so that one can forget the closures and marshal the resulting state git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16683 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08enhance marshallable option for freeze (minor TODO in safe_typing)gareuselesinge
It can be: `Yes Full data, in a state that can be marshalled `No Full data, good for Undo only `Shallow Partial data, marshallable, good for slave processes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16682 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Test for Paral-ITPgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16681 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
The warning output by vernacextend when the classifier is missing is the documentation of this commit: Warning: Vernac entry "Foo" misses a classifier. A classifier is a function that returns an expression of type vernac_classification (see Vernacexpr). You can: - Use '... EXTEND Foo CLASSIFIED AS QUERY ...' if the new vernacular command does not alter the system state; - Use '... EXTEND Foo CLASSIFIED AS SIDEFF ...' if the new vernacular command alters the system state but not the parser nor it starts a proof or ends one; - Use '... EXTEND Foo CLASSIFIED BY f ...' to specify a global function f. The function f will be called passing "Foo" as the only argument; - Add a specific classifier in each clause using the syntax: '[...] => [ f ] -> [...]'. Specific classifiers have precedence over global classifiers. Only one classifier is called. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16680 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Simple machinery to detect EXTEND that interpret during parsinggareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16679 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Support Proof Generalgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16678 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Coqide ported to STMgareuselesinge
Main changes for STM: 1) protocol changed to carry edit/state ids 2) colouring reflects the actual status of every span (evaluated or not) 3) button to force the evaluation of the whole buffer 4) cmd_stack and backtracking completely changed to use state numbers instead of counting sentences 5) feedback messages are completely asynchronous, and the whole protocol could be made so with a minor effort, but there is little point in it right now. Left as a future improvement. Missing bit: add sentence-id to responses of interp command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16677 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Fix testsuite so that it works with STMgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16676 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Manual fixed w.r.t. STMgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16675 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08State Transaction Machinegareuselesinge
The process_transaction function adds a new edge to the Dag without executing the transaction (when possible). The observe id function runs the transactions necessary to reach to the state id. Transaction being on a merged branch are not executed but stored into a future. The finish function calls observe on the tip of the current branch. Imperative modifications to the environment made by some tactics are now explicitly declared by the tactic and modeled as let-in/beta-redexes at the root of the proof term. An example is the abstract tactic. This is the work described in the Coq Workshop 2012 paper. Coq is compile with thread support from now on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Side effect free implementation of admit (Isabelle's oracle)gareuselesinge
new Axiom in Logic.v, proof_admitted : False. admit now simply cases proof_admitted and does not create a new Axiom in the environment. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16673 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Vcs data structure (Git inspired builder for Dag)gareuselesinge
Given named branches, one can incrementally build a Dag using Git like commands git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16672 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Dag data structuregareuselesinge
This is a very simple, only growing, Dag structure with per node optional info and per edge info git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16671 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Searchable stack data structuregareuselesinge
It is like Stack but one can search without popping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16670 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Future library to represent pure computationsgareuselesinge
Since the whole system is imperative, futures are run protecting the global state, and the final state is also saved to let the user freely chain futures. Futures can represent local (lazy) computations or remote ones (delegated). Delegating a future lets a third party assign its value at some poit in the future; in the meanwhile accessing the future value raises an exception. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16669 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Fixing a warning in CoqIDE compilation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16668 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Small fix in IStream interface.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16667 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-07Removing association lists in Constrintern.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16666 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-06Added more flags choice in desambiguating printer. The code isppedrot
parametric on the list of possible flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16665 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-05Tentative fix for bug #2961. When we have to print two terms thatppedrot
should be different, we compute the externalized form for both in the current state. If ever they coincide, we do it again with the implicit arguments flag set. In other words, if those two terms appear the same, we automatically print them with the implicit arguments flag on. This is a bit raw, and we may try other externalization flags, but I assume it to be (almost) sufficient for now. TODO: check every place where we could need such a feature, and try other flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16664 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-04Added test for bug #2846.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16663 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-04Fixing #2846: Uncaught exception Reduction.NotArity.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16662 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-04Added a test for bug #3062.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16661 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-04Fixing #3062. Computation of the value of a fresh identifier wasppedrot
done too early and lead to dynamic conflicts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16660 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-04Removing useless casts between arrays and lists.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16659 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-04Removing now useless merging primitives from Evd.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16658 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-04Small cleaning of printing coercion failures in Ltac interpretation.ppedrot
Now we at least print the type of the offending object. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16657 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-03Small fixes due to the arrival of OCaml 3.12.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16656 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-03Replacing uses of association lists by maps in notations.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16655 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-03Replacing an association list by a map in globalizing environment.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16654 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-02Adding a dependent version of equal_f, thus fixing #3074.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16653 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-02Small typo in Print Debug GCppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16652 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-01Added a Print Debug GC command that displays the current state ofppedrot
the OCaml GC, as indicated by [Gc.stat]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16651 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-01Added a test for bug #3088.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16650 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-01Fixing #3088. Translation from globconstrs to patterns was forgettingppedrot
to register bound variables as such in the return clause. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16649 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-01Documenting the Remove Hints command.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16648 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-01Added printing of instance priority to the Print Instances command.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16647 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-01Documenting the previous commit: Existing Instance with priority.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16646 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-01Granting bug #3098: adding priority to Existing Instances.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16645 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-31Typo in definition clos_reflppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16644 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-30Granting wish #1781:ppedrot
Parenthesis matching on click in all term displays. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16643 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-29Tentative fix for #3054: we refresh universes in a term generatedppedrot
by congruence, as it seems to be done methodically on the remaining of this plugin. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16642 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-29better error message for unexpected renaming (closes #2987)gareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16641 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-29Revert "Only arguments declared as implicit can be renamed"gareuselesinge
This reverts commit 18a89c271d540d794d44e41f50587bb1cad69802. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16640 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-27Protecting every call to current_term in CoqIDE so that callbackppedrot
will not raise an exception if there is no opened tab. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16637 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-27Added a way to change dynamically coqtop arguments in CoqIDE.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16636 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-26Fixing #3089. This implied tweaking the definition of the lexicographicppedrot
product of lists, hence possibly introducing incompatibilities. Parts of the patch by Chantal Keller. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16635 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-26 18:24:13 +0000