aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
| | | | parsing is plugged.
* Do not use ugly Dyn features in the Quote plugin. Use instead theGravatar Pierre-Marie Pédrot2013-11-26
| | | | provided tactic environment to handle open terms.
* Remove the Hiddentac module.Gravatar Arnaud Spiwack2013-11-25
| | | | | | | | Since the new proof engine, Hiddentac has been essentially trivial. Here is what happened to the functions defined there - Aliases, or tactics that were trivial to inline were systematically inlined - Tactics used only in tacinterp have been moved to tacinterp - Other tactics have been moved to a new module Tactics.Simple.
* Field_theory: nicer notations for constants 0 1 ...Gravatar Pierre Letouzey2013-11-21
|
* Add Acc_intro_generator on top of all wf function proof (much much faster ↵Gravatar Julien Forest2013-11-21
| | | | execution)
* bugfix micromega: solved an ambiguous symbol resolutionGravatar fbesson2013-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17092 85f007b7-540e-0410-9357-904b9bb8a0f7
* Porting Tactics.assumption to the new engine.Gravatar ppedrot2013-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17073 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix congruence: normalise hypotheses with respect to evars.Gravatar aspiwack2013-11-02
| | | | | | Detected in CompCert. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17026 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made Proofview.Goal.hyps a named_context.Gravatar aspiwack2013-11-02
| | | | | | There was really no point in having it be a named_context val. The tactics are not going to access the vm cache. Only vm_compute will. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17007 85f007b7-540e-0410-9357-904b9bb8a0f7
* Less use of the list-based interface for goal-bound tactics.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17002 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tachmach.New is now in Proofview.Goal.enter style.Gravatar aspiwack2013-11-02
| | | | | | As a result the use of the glist-style interface for manipulating goals has almost been removed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17001 85f007b7-540e-0410-9357-904b9bb8a0f7
* More Proofview.Goal.enter.Gravatar aspiwack2013-11-02
| | | | | | | | | | Proofview.Goal.enter is meant to eventually replace the Goal.sensitive monad. This commit changes the type of Proofview.Goal.enter from taking a four argument function (environment, evar_map, hyps, concl) from a one argument function of abstract type Proofview.Goal.t. It will be both more extensible and more akin to old-style tactics. This commit also changes the type of Proofview.Goal.{concl,hyps,env} from monadic operations to projection from a Proofview.Goal.t. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17000 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small syntax fix to be compatible with Ocaml 3.11.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16986 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds a new goal selector "all:".Gravatar aspiwack2013-11-02
| | | | | | all:tac applies tac to all the focused subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16982 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).Gravatar aspiwack2013-11-02
| | | | | | | | They were a hack to avoid looking where exceptions were raised and not caught. Hopefully I produce a cleaner stack now, catching errors when it is needed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16980 85f007b7-540e-0410-9357-904b9bb8a0f7
* The tactic [admit] exits with the "unsafe" status.Gravatar aspiwack2013-11-02
| | | | | | | | | | | | | It is highlighted in yellow in Coqide. The unsafe status is tracked throughout the execution of tactics such that nested calls to admit are caught. Many function (mainly those building constr with tactics such as typeclass related stuff, and Function, and a few other like eauto's use of Hint Extern) drop the unsafe status. This is unfortunate, but a lot of refactoring would be in order. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16977 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup of comments.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16976 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plug back the declarative mode.Gravatar aspiwack2013-11-02
| | | | | | It seems to work ok, but I'm not too confident in the long run. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16975 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16971 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of Goal.here, and all the related exceptions and combinators.Gravatar aspiwack2013-11-02
| | | | | | It was a bad idea. The new API based on lists seems more sensible. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On the compilation of Coq, we can see an increase of ~20% compile time on my completely non-scientific tests. Hopefully this can be fixed. There are a lot of low hanging fruits, but this is an iso-functionality commit. With a few exceptions which were not necessary for the compilation of the theories: - The declarative mode is not yet ported - The timeout tactical is currently deactivated because it needs some subtle I/O. The framework is ready to handle it, but I haven't done it yet. - For much the same reason, the ltac debugger is unplugged. It will be more difficult, but will eventually be back. A few comments: I occasionnally used a coercion from [unit Proofview.tactic] to the old [Prooftype.tactic]. It should work smoothely, but loses any backtracking information: the coerced tactics has at most one success. - It is used in autorewrite (it shouldn't be a problem there). Autorewrite's code is fairly old and tricky - It is used in eauto, mostly for "Hint Extern". It may be an issue as time goes as we might want to have various success in a "Hint Extern". But it would require a heavy port of eauto.ml4 - It is used in typeclass eauto, but with a little help from Matthieu, it should be easy to port the whole thing to the new tactic engine, actually simplifying the code. - It is used in fourier. I believe it to be inocuous. - It is used in firstorder and congruence. I think it's ok. Their code is somewhat intricate and I'm not sure they would be easy to actually port. - It is used heavily in Function. And honestly, I have no idea whether it can do harm or not. Updates: (11 June 2013) Pierre-Marie Pédrot contributed the rebase over his new stream based architecture for Ltac matching (r16533), which avoid painfully and expensively working around the exception-throwing control flow of the previous API. (11 October 2013) Rebasing over recent commits (somewhere in r16721-r16730) rendered a major bug in my implementation of Tacticals.New.tclREPEAT_MAIN apparent. It caused Field_theory.v to loop. The bug made rewrite !lemma, rewrite ?lemma and autorewrite incorrect (tclREPEAT_MAIN was essentially tclREPEAT, causing rewrites to be tried in the side-conditions of conditional rewrites as well). The new implementation makes Coq faster, but it is pretty much impossible to tell if it is significant at all. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16967 85f007b7-540e-0410-9357-904b9bb8a0f7
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
| | | | | | | | | | | To reduce the amount of syntactic noise, we now provide a few inner modules Int.List, Id.List, String.List, Sorts.List which contain some monomorphic (or semi-monomorphic) functions such as mem, assoc, ... NB: for Int.List.mem and co we reuse List.memq and so on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rtree : cleanup of the comparing codeGravatar letouzey2013-10-24
| | | | | | | | | * Using generic fold functions was unecessarily obscure * No more List.mem and hence indirect use of ocaml generic comparison * Rtree.equiv (former Rtree.compare_rtree) has now a less cryptic semantic... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16934 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oups, repair the compilation (micromega + Morphism_prop)Gravatar letouzey2013-10-24
| | | | | | | | | | | | | It seems I forgot to fully recompile after my last bunch of syntactic changes about List.assoc_f, that weren't so syntactic after all, sorry : - Util isn't used in micromega, hence no List.assoc_f there - There is something wrong in my modifications of Notation_ops that breaks the compilation of Morphism_prop. For the moment I don't see what, so I revert all the modifications of this file git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16930 85f007b7-540e-0410-9357-904b9bb8a0f7
* Get rid of polymorphic comparison in "plugins/btauto/refl_btauto.ml".Gravatar xclerc2013-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16927 85f007b7-540e-0410-9357-904b9bb8a0f7
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
* cList: a few alternative to hashtbl-based uniquize, distinct, subsetGravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16921 85f007b7-540e-0410-9357-904b9bb8a0f7
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
* declaration_hooks use EphemeronGravatar gareuselesinge2013-10-18
| | | | | | | | Ideally, any component of the global state that is a function or any other unmarshallable data should be stocked as an ephemeron to make the state always marshallable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16893 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reintroduce "or" instead of "||" as the latter is redifined in "sos_lib.ml" ↵Gravatar xclerc2013-10-16
| | | | | | with a different semantics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16888 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid polymorphic comparison (plugins/rtauto).Gravatar xclerc2013-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16886 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid polymorphic comparison (plugins/cc).Gravatar xclerc2013-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16885 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove some uses of local modules (some were unused, some were costly).Gravatar xclerc2013-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16883 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of the use of deprecated elements (from the OCaml standard library).Gravatar xclerc2013-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
| | | | | | | | | | | | | | | | | | | state out of one we were threading all the way along. This should be safer, as one cannot forego side effects accidentally by manipulating explicitly the [sigma] container. Still, this patch raised the issue of badly used evar maps. There is an ad-hoc workaround (i.e. a hack) in Rewrite to handle the fact it uses evar maps in an unorthodox way. Likewise, that mean we have to revert all contrib patches that added effect threading... There was also a dubious use of side effects in their toplevel handling, that duplicates them, leading to the need of a rather unsafe List.uniquize afterwards. It should be investigaged. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16850 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: better handle proof modesGravatar gareuselesinge2013-09-30
| | | | | | | | Proof modes are really spaghetti code. It is a global state that you can't access (held by G_vernac). We stick it to the branches... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16820 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵Gravatar xclerc2013-09-19
| | | | | | with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
| | | | | | | | | | | | casts of ints to evars. - 2 in Evarutil and Goal which are really needed, even though the Goal one could (and should) be removed; - 2 in G_xml and Detyping that are there for completeness sake, but that might be made anomalies altogether; - 1 in Newring which is quite dubious at best, and should be fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16786 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing more association lists in Constrintern.Gravatar ppedrot2013-09-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16757 85f007b7-540e-0410-9357-904b9bb8a0f7
* add "Print Ring" and "Print Field" vernacular commandsGravatar gareuselesinge2013-08-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16751 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing the code of field_simplify_eq.Gravatar amahboub2013-08-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16749 85f007b7-540e-0410-9357-904b9bb8a0f7
* recdef: restore old semantics (pre STM)Gravatar gareuselesinge2013-08-30
| | | | | | | | The Stm commit switched from an home made handling of failures to a with_state_protection. This was wrong, since in case of success the global state has to be left altered. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16746 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix typo in error messageGravatar gareuselesinge2013-08-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16745 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
| | | | | | | | | | The extended signature is defined in CMap, and should be compatible with the old one, except that module arguments have to be explicitely named. The implementation itself is quite unsafe, as it relies on the current implementation of OCaml maps, even though that should not be a problem (it has not changed in ages). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing an incompleteness of the ring/field tacticsGravatar amahboub2013-08-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The problem occurs when a customized ring/field structure declared with a so-called "morphism" (see 24.5 in the manual) tactic allowing to reify (numerical) constants efficiently. When declaring a ring/field structure, the user can provide a cast function phi in order to express numerical constants in another type than the carrier of the ring. This is useful for instance when the ring is abstract (like the type R of reals) and one needs to express constants to large to be parsed in unary representation (for instance using a phi : Z -> R). Formerly, the completeness of the tactic required (phi 1) (resp. (phi 0)) to be convertible to 1 (resp. 0), which is not the case when phi is opaque. This was not documented untill recently but I moreover think this is also not desirable since the user can have good reasons to work with such an opaque case phi. Hence this commit: - adds two constructors to PExpr and FExpr for a correct reification - unplugs the optimizations in reification: optimizing reification is much less efficient than using a cast known to the tactic. TODO : It would probably be worth declaring IZR as a cast in the ring/field tactics provided for Reals in the std lib. The completeness of the tactic formerly relied on the fact that git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16730 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correcting misplaced Proof command.Gravatar amahboub2013-08-22
| | | | | | | | | I did not even know it was possible to inline a 'Proof.' anywhere in a script. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16729 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing a significant efficiency leak in the code of the field tactic.Gravatar amahboub2013-08-22
| | | | | | | | | | | | | | | | | | | | | | | | The field tactic post-processes the data generated during normalization to ensure that vanished denominators do not cancel: essentially, this step removes duplicates from a list of polynomials and uses the clean list to generate the conjunction of associated non-zero conditions. This conjunction is the proof obligation the user has to prove by hand after a successful call to the field tactic. The computation of the proof obligation statement was performed using a fine-tuned reduction strategy, coded in the newring.ml4 file (see the fv-protect tactic). However, not only this strategy information was forgotten by the kernel, but the strategy used at Qed time caused a real explosion (examples normalized in 70s by the tactic have a one hour Qed). No idea why. The fix consists in opacifying the part of the goal irrelevant to computation and call the vm on the duplicate removal step. BTW this step is programmed in a naive way and can probably be made more efficient. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16728 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 11:13:01 +0000