aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* 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 ```
* Don't double up on periods in anomaliesGravatar Jason Gross2017-06-02
| | | | | | | | We don't want "Anomaly: Returned a functional value in a type not recognized as a product type.. Please report at http://coq.inria.fr/bugs/." but instead "Anomaly: Returned a functional value in a type not recognized as a product type. Please report at http://coq.inria.fr/bugs/."
* Merge PR#515: extract "plugins/micromega/micromega.ml{,i}" files from ↵Gravatar Maxime Dénès2017-06-02
|\ | | | | | | "plugins/micromega/MExtraction.v"
* \ Merge PR#696: Trunk+cleanup constr of globalGravatar Maxime Dénès2017-06-01
|\ \
* \ \ Merge PR#561: Improving the Name APIGravatar Maxime Dénès2017-06-01
|\ \ \
| | | * Break circular dependency in MExtractionGravatar Jason Gross2017-06-01
| | | | | | | | | | | | | | | | Described in https://github.com/coq/coq/pull/515#discussion_r119230833
| | | * extract "plugins/micromega/micromega.ml{,i}" files from ↵Gravatar Matej Kosik2017-06-01
| |_|/ |/| | | | | | | | "plugins/micromega/MExtraction.v"
| * | Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This module collects the functions of Nameops which are about Name.t and somehow standardize or improve their name, resulting in particular from discussions in working group. Note the use of a dedicated exception rather than a failwith for Nameops.Name.out. Drawback of the approach: one needs to open Nameops, or to use long prefix Nameops.Name.
* | | Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
| | | | | | | | | | | | | | | | | | | | | | | | This allows a better control on the name to give to an evar and, in particular, to address the issue about naming produced by "epose proof" in one of the comment of Zimmi48 at PR #248 (see file names.v). Incidentally updating output of Show output test (evar numbers shifted).
* | | Adding "epose", "eset", "eremember" which allow to set terms withGravatar Hugo Herbelin2017-05-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | evars. This is for consistency with the rest of the language. For instance, "eremember" and "epose" are supposed to refer to terms occurring in the goal, hence not leaving evars, hence in general pointless. Eventually, I guess that "e" should be a modifier (see e.g. the discussion at #3872), or the difference is removed.
* | | Adding "eassert", "eenough", "epose proof", which allow to stateGravatar Hugo Herbelin2017-05-30
|/ / | | | | | | a goal with unresolved evars.
* | Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Maxime Dénès2017-05-30
|\ \
| | * Ltac cleanup: no more constr_of_global callsGravatar Matthieu Sozeau2017-05-29
| | |
| | * Equality cleanup: remove constr_of_globalGravatar Matthieu Sozeau2017-05-29
| | |
| | * 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
|\ \
* \ \ Merge PR#678: [coqlib] Move `Coqlib` to `library/`.Gravatar Maxime Dénès2017-05-28
|\ \ \
| | | * Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Gaëtan Gilbert2017-05-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Deprecations which can't be fixed in 4.02.3 are locally wrapped with [@@@ocaml.warning "-3"]. The only ones encountered are - capitalize to capitalize_ascii and variants. Changing to ascii would break coqdoc -latin1 and maybe other things though. - external "noalloc" to external [@@noalloc]
* | | | Merge PR#675: [coqlib] Deprecate redundant Coqlib functions.Gravatar Maxime Dénès2017-05-28
|\ \ \ \
| | | * | [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.
| * / [coqlib] Deprecate redundant Coqlib functions.Gravatar Emilio Jesus Gallego Arias2017-05-27
| |/ | | | | | | | | | | | | | | | | | | | | | | We remove redundant functions `coq_constant`, `gen_reference`, and `gen_constant`. This is a first step towards a lazy binding of libraries references. We have also chosen to untangle `constr` from `Coqlib`, as how to instantiate the reference (in particular wrt universes) is a client-side issue. (The client may want to provide an `evar_map` ?) c.f. #186
* / Exporting a few primitive tacticals as named Ltac definitions.Gravatar Pierre-Marie Pédrot2017-05-27
|/
* Merge PR#666: romega revisited : no more normalization trace, cleaned-up ↵Gravatar Maxime Dénès2017-05-26
|\ | | | | | | resolution trace
* \ Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsGravatar Maxime Dénès2017-05-25
|\ \
* \ \ Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\ \ \
* \ \ \ Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \ \ \
* \ \ \ \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \ \ \ \
| | | | | * ROmega: division-aware ReflOmegaCore, allowing trace without termsGravatar Pierre Letouzey2017-05-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The trace only mentions the constant k by which we want to divide the equation, not anymore the equation we obtain after the division. Shorter trace, and it won't take much more time to perform the few Z.div than checking as currently the equality of the initial equation and the final equation multiplied by k.
| | * | | | [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
| | | | |
| | | | * refl_omega.v: explicitely identify atom indexes and omega varsGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * ReflOmegaCore: misc cleanup, <? instead of bgt, etcGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * ROmega : O_STATE turned into a O_SUMGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We benefit from the fact that we normalize now *all* hypotheses even the one defining the "stated" variable: it is produced as ...def of v... = v and normalized as -v + ...def of v... = 0 which is precisely what we should add to the initial equation during a O_STATE.
| | | | * ROmega: less contructors in the final omega traceGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now that O_SUM is properly optimized (cf. the [fusion] function), we could use it to encode CONTRADICTION and NEGATE_CONTRADICT(_INV). This way, the trace has almost the same size, but ReflOmegaCore.v is shorter and easier to maintain.
| | | | * ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANTGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * ReflOmegaCore: reverse some integer mult (coefs k1,k2 will often be simple)Gravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * ReflOmegaCore: comment, reorganize, permut some constructors, etcGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * romega: add a tactic named unsafe_romega (for debugging, or bold users)Gravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In this variant, the proof term produced by romega isn't verified at the tactic run-time (no vm_compute). In theory, [unsafe_romega] should behave exactly as [romega], but faster. Now, if there's a bug in romega, we'll be notified only at the following Qed. This could be interesting for debugging purpose : you could inspect the produced buggish term via a Show Proof.
| | | | * romega: no more normalization trace, replaced by some Coq-side computationGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a major change : - Generated proofs are quite shorter, since only the resolution trace remains. - No time penalty mesured (it even tends to be slightly faster this way). - Less infrastructure in ReflOmegaCore and refl_omega. - Warning: the normalization functions in ML and in Coq should be kept in sync, as well as the variable order. - Btw: get rid of ML constructor Oufo
| | | | * romega/const_omega : a few improvements (less try with, no gen equality)Gravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * romega: use N instead of nat for TvarGravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In a coming commit, we'll normalize terms by a Coq function that will compare Tvar's instead of blindly applying a trace, so let's speed-up these comparisons.
| | | | * romega: shorter trace (no more term lengths)Gravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * refl_omega: refactoring of normalize_equationGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * ReflOmegaCore: lots of dead code + a few refactored proofsGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * romega: if it bugs again, at least do it with a short and quick errorGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * refl_omega: comment the lack of lifts when dealing with arrowsGravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * romega: discard constructor D_mono (shorter trace + fix a bug)Gravatar Pierre Letouzey2017-05-22
| | | | | | | | | | | | | | | | | | | | For the bug, see new test test_romega10 in test-suite/success/ROmega0.v.
| | | | * refl_omega: more refactoring (e.g. IntSets instead of sorted lists)Gravatar Pierre Letouzey2017-05-22
| | | | |
| | | | * refl_omega: refactoring (e.g. useless args in destructurate_pos_hyp)Gravatar Pierre Letouzey2017-05-22
| | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 21:16:13 +0000