aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/omega
Commit message (Collapse)AuthorAge
* Using is_conv rather than eq_constr to find `nat` or `Z` in omega.Gravatar Hugo Herbelin2017-11-23
| | | | | | | | | | Moving at the same to a passing "env sigma" style rather than passing "gl". Not that it is strictly necessary, but since we had to move functions taking only a "sigma" to functions taking also a "env", we eventually adopted the "env sigma" style. (The "gl" style would have been as good.) This answers wish #4717.
* Omega now aware of context variables with bodies (in type Z or nat) (fix bug ↵Gravatar Pierre Letouzey2017-10-05
| | | | | | | | | | | | 148) For compatibility, this extra feature of omega could be disabled via Unset Omega UseLocalDefs. Caveat : for now, real let-ins inside goals or hyps aren't handled, use some "cbv zeta" reduction if you want to get rid of them. And context definitions whose types aren't Z or nat are ignored, some manual "unfold" are still mandatory if expanding these definitions will help omega.
* Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
| | | | | The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
* Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Guillaume Melquiond2017-09-12
|
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Merge PR#673: Two fixes about zify (bugs #5336 and #5439)Gravatar Maxime Dénès2017-06-14
|\
* | Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
| |
* | Explicit the unsafe flag of all calls to Refine.refine.Gravatar Pierre-Marie Pédrot2017-06-13
| |
* | Merge PR#718: API cleanup: aliasesGravatar Maxime Dénès2017-06-12
|\ \
| | * zify: force reduction of (Z.max 0 0) and similar (fix #5439)Gravatar Pierre Letouzey2017-06-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | Turn some "simpl" into "compute". Also do the same for the few "simpl (Z.of_nat ...)". This way, definition like Z.max are properly reduced, and moreover zify isn't sensible anymore to the "Arguments Z.of_nat : simpl never" that some user want (see also #5039). Unfortunately, the compute we're using now still honor the "Opaque" declarations, so a "Opaque Z.max" will block things again (see also #5374).
| | * zify: confusion between Pos2Z.inj_sub and Pos2Z.inj_sub_max (fix #5336)Gravatar Pierre Letouzey2017-06-12
| |/ |/|
* | Remove remaining vo.itarget files (obsolete since PR #499)Gravatar Pierre Letouzey2017-06-10
| |
| * Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \ | |/ |/|
* | Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
| |
* | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Reminder of (some of) the reasons for removal: - Despite the claim in sigma.mli, it does *not* prevent evar leaks, something like: fun env evd -> let (evd',ev) = new_evar env evd in (evd,ev) will typecheck even with Sigma-like type annotations (with a proof of reflexivity) - The API stayed embryonic. Even typing functions were not ported to Sigma. - Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly less unsafe ones (e.g. s_enter), but those ones were not marked unsafe at all (despite still being so). - There was no good story for higher order functions manipulating evar maps. Without higher order, one can most of the time get away with reusing the same name for the updated evar map. - Most of the code doing complex things with evar maps was using unsafe casts to sigma. This code should be fixed, but this is an orthogonal issue. Of course, this was showing a nice and elegant use of GADTs, but the cost/benefit ratio in practice did not seem good.
* | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
| * Fix bug #5019 (looping zify on dependent types)Gravatar Jason Gross2017-06-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes [bug #5019](https://coq.inria.fr/bugs/show_bug.cgi?id=5019), "[zify] loops on dependent types"; before, we would see a `Z.of_nat (S ?k)` which could not be turned into `Z.succ (Z.of_nat k)`, add a hypothesis of the shape `0 <= Z.of_nat (S k)`, turn that into a hypothesis of the shape `0 <= Z.succ (Z.of_nat k)`, and loop forever on this. This may not be the "right" fix (there may be cases where `zify` should succeed where it still fails with this change), but this is a pure bugfix in the sense that the only places where it changes the behavior of `zify` are the places where, previously, `zify` looped forever.
| * Omega: use "simpl" only on coefficents, not on atoms (fix #4132)Gravatar Pierre Letouzey2017-05-29
| | | | | | | | | | | | | | | | | | | | | | Two issues in one: - some focused_simpl were called on the wrong locations - some focused_simpl were done on whole equations In the two cases, this could be bad if "simpl" goes too far with respect to what omega expects: later calls to "occurrence" might fail. This may happen for instance if an atom isn't a variable, but a let-in (b:=5:Z in the example).
* | Cleanup: removal of constr_of_global.Gravatar Matthieu Sozeau2017-05-29
| | | | | | | | | | | | Constrintern.pf_global returns a global_reference, not a constr, adapt plugins accordingly, properly registering universes where necessary.
* | Merge PR#512: [cleanup] Unify all calls to the error function.Gravatar Maxime Dénès2017-05-29
|\ \
| * | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
* | | [coqlib] Move `Coqlib` to `library/`.Gravatar Emilio Jesus Gallego Arias2017-05-27
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We move Coqlib to library in preparation for the late binding of Gallina-level references. Placing `Coqlib` in `library/` is convenient as some components such as pretyping need to depend on it. By moving we lose the ability to locate references by syntactic abbreviations, but IMHO it makes to require ML code to refer to a true constant instead of an abbreviation/notation. Unfortunately this change means that we break the `Coqlib` API (providing a compatibility function is not possible), however we do so for a good reason. The main changes are: - move `Coqlib` to `library/`. - remove reference -> term from `Coqlib`. In particular, clients will have different needs with regards to universes/evar_maps, so we force them to call the (not very safe) `Universes.constr_of_global` explicitly so the users are marked. - move late binding of impossible case from `Termops` to `pretying/Evarconv`. Remove hook. - `Coqlib.find_reference` doesn't support syntactic abbreviations anymore. - remove duplication of `Coqlib` code in `Program`. - remove duplication of `Coqlib` code in `Ltac.Rewrite`. - A special note about bug 5066 and commit 6e87877 . This case illustrates the danger of duplication in the code base; the solution chosen there was to transform the not-found anomaly into an error message, however the general policy was far from clear. The long term solution is indeed make `find_reference` emit `Not_found` and let the client handle the error maybe non-fatally. (so they can test for constants.
* | Merge PR#666: romega revisited : no more normalization trace, cleaned-up ↵Gravatar Maxime Dénès2017-05-26
|\ \ | | | | | | | | | resolution trace
* | | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
| * | refl_omega: some code refactoringGravatar Pierre Letouzey2017-05-22
| | |
| * | ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANTGravatar Pierre Letouzey2017-05-22
|/ /
* | Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| |
* | Porting omega to the new tactic API.Gravatar Pierre-Marie Pédrot2017-04-24
| |
* | Removing trivial compatibility layer in omega.Gravatar Pierre-Marie Pédrot2017-04-24
| |
* | Fix an unhandled exception in Omega.Gravatar Pierre-Marie Pédrot2017-04-07
| |
* | Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
| | | | | | | | | | For now we only normalize sorts, and we leave instances for the next commit.
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\ \
| * | Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
| | | | | | | | | | | | | | | | | | | | | This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements.
* | | Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | Now they are useless because all of the primitives are (should?) be evar-insensitive.
* | | Fix a mishandled exception in Omega.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | Due to the introduction of the monadic layer, an exception was raised at a later time and not caught properly.
* | | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | | | | | | | This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr.
* | | Omega API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Contradiction API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|/ /
* | Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
| | | | | | | | | | | | There was no reason to keep them separate since quite a long time. Historically, they were making Genarg depend or not on upper strata of the code, but since it was moved to lib/ this is not justified anymore.
* | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| | | | | | | | | | | | | | | | | | | | | | mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions. If multiple modules define a function with a same name, e.g.: Context.{Rel,Named}.get_type those calls were prefixed with a corresponding prefix to make sure that it is obvious which function is being called.
* | CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-24
|/
* 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