aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring
Commit message (Collapse)AuthorAge
* Ncring_initial: avoid a notation overridingGravatar Pierre Letouzey2016-09-29
|
* Ring_theory: avoid overriding a few notationsGravatar Pierre Letouzey2016-09-28
|
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
| | | | For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a reimplementation of Hugo's PR#117. We are trying to address the problem that the name of some reduction functions was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in reduction). Like PR#117, we are careful that no function changed semantics without changing the names. Porting existing ML code should be a matter of renamings a few function calls. Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX collectively denominated iota. We renamed the following functions: Closure.betadeltaiota -> Closure.all Closure.betadeltaiotanolet -> Closure.allnolet Reductionops.beta -> Closure.beta Reductionops.zeta -> Closure.zeta Reductionops.betaiota -> Closure.betaiota Reductionops.betaiotazeta -> Closure.betaiotazeta Reductionops.delta -> Closure.delta Reductionops.betalet -> Closure.betazeta Reductionops.betadelta -> Closure.betadeltazeta Reductionops.betadeltaiota -> Closure.all Reductionops.betadeltaiotanolet -> Closure.allnolet Closure.no_red -> Closure.nored Reductionops.nored -> Closure.nored Reductionops.nf_betadeltaiota -> Reductionops.nf_all Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta Reductionops.whd_betadeltaiota -> Reductionops.whd_all Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state Reductionops.whd_eta -> Reductionops.shrink_eta Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all And removed the following ones: Reductionops.whd_betaetalet Reductionops.whd_betaetalet_stack Reductionops.whd_betaetalet_state Reductionops.whd_betadeltaeta_stack Reductionops.whd_betadeltaeta_state Reductionops.whd_betadeltaeta Reductionops.whd_betadeltaiotaeta_stack Reductionops.whd_betadeltaiotaeta_state Reductionops.whd_betadeltaiotaeta They were unused and having some reduction functions perform eta is confusing as whd_all and nf_all don't do it.
* Removing tactic compatibility layers in setoid_ring.Gravatar Pierre-Marie Pédrot2016-06-24
|
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There were three versions of injection: 1. "injection term" without "as" clause: was leaving hypotheses on the goal in reverse order 2. "injection term as ipat", first version: was introduction hypotheses using ipat in reverse order without checking that the number of ipat was the size of the injection (activated with "Unset Injection L2R Pattern Order") 3. "injection term as ipat", second version: was introduction hypotheses using ipat in left-to-right order checking that the number of ipat was the size of the injection and clearing the injecting term by default if an hypothesis (activated with "Set Injection L2R Pattern Order", default one from 8.5) There is now: 4. "injection term" without "as" clause, new version: introducing the components of the injection in the context in left-to-right order using default intro-patterns "?" and clearing the injecting term by default if an hypothesis (activated with "Set Structural Injection") The new versions 3. and 4. are the "expected" ones in the sense that they have the following good properties: - introduction in the context is in the natural left-to-right order - "injection" behaves the same with and without "as", always introducing the hypotheses in the goal what corresponds to the natural expectation as the changes I made in the proof scripts for adaptation confirm - clear the "injection" hypothesis when an hypothesis which is the natural expectation as the changes I made in the proof scripts for adaptation confirm The compatibility can be preserved by "Unset Structural Injection" or by calling "simple injection". The flag is currently off.
* Adding printers for ring and field commands.Gravatar Hugo Herbelin2016-06-16
|
* Remove inappropriate comment.Gravatar Maxime Dénès2016-06-16
|
* Merge remote-tracking branch 'github/evarunsafe' into trunkGravatar Matthieu Sozeau2016-06-14
|\
| * newring: fix for hack using evars as integers.Gravatar Matthieu Sozeau2016-06-09
| |
* | Compilation via pack for plugins of the stdlibGravatar Pierre Letouzey2016-06-08
|/ | | | | | | | | | | | | | | | | | | | | | | | For now, the pack name reuse the previous .cma name of the plugin, (extraction_plugin, etc). The earlier .mllib files in plugins are now named .mlpack. They are also handled by bin/ocamllibdep, just as .mllib. We've slightly modified ocamllibdep to help setting the -for-pack options: in *.mlpack.d files, there are some extra variables such as foo/bar_FORPACK := -for-pack Baz when foo/bar.ml is mentioned in baz.mlpack. When a plugin is calling a function from another plugin, the name need to be qualified (Foo_plugin.Bar.baz instead of Bar.baz). Btw, we discard the generated files plugins/*/*_mod.ml, they are obsolete now, replaced by DECLARE PLUGIN. Nota: there's a potential problem in the micromega directory, some .ml files are linked both in micromega_plugin and in csdpcert. And we now compile these files with a -for-pack, even if they are not packed in the case of csdpcert. In practice, csdpcert seems to work well, but we should verify with OCaml experts.
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
|
* Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
|
* Revert "Adding printers for ring and field commands."Gravatar Hugo Herbelin2016-04-27
| | | | This reverts commit 9df1a3cf26d78df507d0e35c2d9ca987151777be.
* Adding printers for ring and field commands.Gravatar Hugo Herbelin2016-04-27
|
* Getting rid of the "_mods" parsing entry.Gravatar Pierre-Marie Pédrot2016-04-01
| | | | | | It was only used by setoid_ring for the Add Ring command, and was easily replaced by a dedicated argument. Moreover, it was of no use to tactic notations.
* Removing the special status of generic entries defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
| | | | | | | | | | | The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there.
* Removing useless grammar.cma dependencies.Gravatar Pierre-Marie Pédrot2016-03-06
|
* Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
|
* The tactic generic argument now returns a value rather than a glob_expr.Gravatar Pierre-Marie Pédrot2016-02-22
| | | | | | | | | | The glob_expr was actually always embedded as a VFun, so this patch should not change anything semantically. The only change occurs in the plugin API where one should use the Tacinterp.tactic_of_value function instead of Tacinterp.eval_tactic. Moreover, this patch allows to use tactics returning arguments from the ML side.
* Moving conversion functions to the new tactic API.Gravatar Pierre-Marie Pédrot2016-02-15
|
* Renaming functions in Typing to stick to the standard e_* scheme.Gravatar Pierre-Marie Pédrot2016-02-15
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | External tactics and notations now accept any tactic argument.Gravatar Pierre-Marie Pédrot2015-12-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit has deep consequences in term of tactic evaluation, as it allows to pass any tac_arg to ML and alias tactics rather than mere generic arguments. This makes the evaluation much more uniform, and in particular it removes the special evaluation function for notations. This last point may break some notations out there unluckily. I had to treat in an ad-hoc way the tactic(...) entry of tactic notations because it is actually not interpreted as a generic argument but rather as a proper tactic expression instead. There is for now no syntax to pass any tactic argument to a given ML or notation tactic, but this should come soon. Also fixes bug #3849 en passant.
* | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-08
|\|
| * Fix some typos.Gravatar Guillaume Melquiond2015-12-07
| |
* | Getting rid of dynamic hacks in Setoid_newring.Gravatar Pierre-Marie Pédrot2015-12-04
| |
* | Removing the last use of tacticIn in setoid_ring.Gravatar Pierre-Marie Pédrot2015-12-03
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\|
| * Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
| | | | | | | | | | Keep user-side information on the names used in instances of universe polymorphic references and use them for printing.
* | Proofview.Goal.sigma returns an indexed evarmap.Gravatar Pierre-Marie Pédrot2015-10-20
| |
* | Boxing the Goal.enter primitive into a record type.Gravatar Pierre-Marie Pédrot2015-10-20
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\|
| * Univs: fix evar_map initialization in newring.Gravatar Matthieu Sozeau2015-10-02
| |
* | Merge v8.5 into trunkGravatar Hugo Herbelin2015-05-15
|\| | | | | | | | | | | | | Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
| * Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Some functions from pretyping/typing.ml and their derivatives were potential source of evarmap leaks, as they dropped their resulting evarmap. This commit clarifies the situation by renaming them according to a unsafe_* scheme. Their sound variant is likewise renamed to their old name. The following renamings were made. - Typing.type_of -> unsafe_type_of - Typing.e_type_of -> type_of - A new e_type_of function that matches the e_ prefix policy - Tacmach.pf_type_of -> pf_unsafe_type_of - A new safe pf_type_of function. All uses of unsafe_* functions should be eventually eliminated.
| * Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Gravatar Hugo Herbelin2015-02-12
| | | | | | | | This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767.
| * Capital letter in plugins.Gravatar Hugo Herbelin2015-02-12
| |
* | Adding a proper interface to Newring.Gravatar Pierre-Marie Pédrot2015-01-25
| | | | | | | | | | The ring ASTs were put in a separate interface, and only the extension-related code was put in a dedicated G_newring file.
* | Embedding the index of the ML tactic entry in the Tacexpr AST.Gravatar Pierre-Marie Pédrot2015-01-21
|/ | | | | This will allow to get rid of the fragile mechanism of discriminating which entry to call depending on the dynamic type of its arguments.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Feedback message: hold extra info to help routingGravatar Enrico Tassi2014-10-31
| | | | | PIDE based GUIs can take advantage of multiple panels and get some feedback routed there. E.g. query panel
* Removing an Evd.merge in Newring.Gravatar Pierre-Marie Pédrot2014-10-27
|
* Fix some typos in comments.Gravatar Guillaume Melquiond2014-10-27
|
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
| | | | The Unsafe module is for unsafe tactics which cannot be done without anytime soon. Whereas V82 indicates a function which we want to get rid of and that shouldn't be used in a new function.
* Fix cbn behavior wrt simpl no matchGravatar Pierre Boutillier2014-10-01
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 17:35:10 +0000