aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
...
| | * | A fix for #5598 (no discharge of Existing Classes referring to local variables).Gravatar Hugo Herbelin2017-06-28
| | | |
| | * | Avoiding an optional int rather than using -1 to encode a local flag.Gravatar Hugo Herbelin2017-06-28
| |/ / |/| | | | | | | | | | | | | | Also giving the proper local flag to the hint registration, even on a Global instance, since the instance discharge manage itself the redefinition of a hint.
| | * Addressing #5434 (ltac pattern-matching refusing to match anonymous variables).Gravatar Hugo Herbelin2017-06-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Ltac pattern-matching was requiring dependent variables to be named. This "natural" expectation is however not guaranteed by unification: an evar can be dependent on an anonymous variable, resulting in elaborated terms with dependent anonymous variables (see example in file 5434.v). This commit "fixes" the problem by not requiring that dependent variables are named in ltac pattern-matching. Ltac pattern-matching names itself these anonymous dependent variables, using the same strategy as the printer (i.e. using "H" to display such internally-anonymous dependent variables).
* | | Fix a bug in cumulativityGravatar Amin Timany2017-06-16
| | |
* | | Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
| | |
* | | Fix a bugGravatar Amin Timany2017-06-16
| | | | | | | | | | | | | | | Incorrect environment was used when checking subtyping information of inductive types.
* | | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
| | |
* | | Fix bugsGravatar Amin Timany2017-06-16
| | |
* | | Squashed commit of the following:Gravatar Amin Timany2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Except I have disabled the minimization of universes after sections as it seems to interfere with the STM machinery causing files like test-suite/vio/print.v to loop when processed asynchronously. This is very peculiar and needs more investigation as the aforementioned file does not have any sections or any universe polymorphic definitions! commit fc785326080b9451eb4700b16ccd3f7df214e0ed Author: Amin Timany <amintimany@gmail.com> Date: Mon Apr 24 17:14:21 2017 +0200 Revert STL to monomorphic commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996 Author: Amin Timany <amintimany@gmail.com> Date: Mon Apr 24 17:02:42 2017 +0200 Try unifying universes before apply subtyping commit ff393742c37b9241c83498e84c2274967a1a58dc Author: Amin Timany <amintimany@gmail.com> Date: Sun Apr 23 13:49:04 2017 +0200 Compile more of STL with universe polymorphism commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6 Author: Amin Timany <amintimany@gmail.com> Date: Tue Apr 18 21:26:45 2017 +0200 Made more progress on compiling the standard library commit b8550ffcce0861794116eb3b12b84e1158c2b4f8 Author: Amin Timany <amintimany@gmail.com> Date: Sun Apr 16 22:55:19 2017 +0200 Make more number theoretic modules monomorphic commit 29d126d4d4910683f7e6aada2a25209151e41b10 Author: Amin Timany <amintimany@gmail.com> Date: Fri Apr 14 16:11:48 2017 +0200 WIP more of standard library compiles Also: Matthieu fixed a bug in rewrite system which was faulty when introducing new morphisms (Add Morphism) command. commit 23bc33b843f098acaba4c63c71c68f79c4641f8c Author: Amin Timany <amintimany@gmail.com> Date: Fri Apr 14 11:39:21 2017 +0200 WIP: more of the standard library compiles We have implemented convertibility of constructors up-to mutual subtyping of their corresponding inductive types. This is similar to the behavior of template polymorphism. commit d0abc5c50d593404fb41b98d588c3843382afd4f Author: Amin Timany <amintimany@gmail.com> Date: Wed Apr 12 19:02:39 2017 +0200 WIP: trying to get the standard library compile with universe polymorphism We are trying to prune universes after section ends. Sections add a load of universes that are not appearing in the body, type or the constraints.
* | | Make unification use subtyping info of inductivesGravatar Amin Timany2017-06-16
| | |
* | | Use inductive subtyping for conv/cumulGravatar Amin Timany2017-06-16
| | |
* | | Subtyping inference for inductoves and recordsGravatar Amin Timany2017-06-16
| | | | | | | | | | | | Also reinferred after sections discharge
* | | Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
| |/ |/| | | | | | | | | | | | | | | It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping.
| * Merge PR#713: Bump year in headers.Gravatar Maxime Dénès2017-06-15
| |\
| * \ Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Maxime Dénès2017-06-15
| |\ \
* | \ \ Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\ \ \ \
* \ \ \ \ Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\ \ \ \ \
| | * | | | Deprecate options that were introduced for compatibility with 8.2.Gravatar Guillaume Melquiond2017-06-14
| | | | | |
| | * | | | Remove options deprecated since 8.4.Gravatar Guillaume Melquiond2017-06-14
| | | | | |
| | * | | | Remove support for Coq 8.3.Gravatar Guillaume Melquiond2017-06-14
| | | | | |
| | * | | | Remove support for Coq 8.2.Gravatar Guillaume Melquiond2017-06-14
| |/ / / / |/| | | |
* | | | | Merge PR#714: Print feature Proof-of-Concept (episode 2)Gravatar Maxime Dénès2017-06-13
|\ \ \ \ \
| | * | | | A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
| |/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let".
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \ \ \ \ | | |/ / / | |/| | |
* | | | | 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.
* | | | | Merge PR#716: Don't double up on periods in anomaliesGravatar Maxime Dénès2017-06-06
|\ \ \ \ \
* \ \ \ \ \ Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ↵Gravatar Maxime Dénès2017-06-05
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | a flag suspectingly renamed in a clearer way
| | | | | * | Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Matthieu Sozeau2017-06-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Use an explicit label ~algebraic for make_flexible_variable as well.
| | | | * | | Added support for a side effect on constants in reduction functions.Gravatar Thomas Sibut-Pinote2017-06-04
| |_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This exports two functions: - declare_reduction_effect: to declare a hook to be applied when some constant are visited during the execution of some reduction functions (primarily cbv, but also cbn, simpl, hnf, ...). - set_reduction_effect: to declare a constant on which a given effect hook should be called. Developed jointly by Thomas Sibut-Pinote and Hugo Herbelin. Added support for printing effect in functions of tacred.ml.
| | * | | | 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#670: Postponing of universe constraints unification in term equality.Gravatar Maxime Dénès2017-06-01
|\ \ \ \ \
* \ \ \ \ \ 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
|\ \ \ \ \ \ \
| | | | | | | * Bump year in headers.Gravatar Maxime Dénès2017-06-01
| | | | | | | |
* | | | | | | | Merge PR#694: Fixing #5523 (missing support for complex constructions in ↵Gravatar Maxime Dénès2017-06-01
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | recursive notations) (bis)
| | | | | | * \ \ Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake ↵Gravatar Maxime Dénès2017-05-31
| | | | | | |\ \ \ | | | | | | | |_|/ | | | | | | |/| | | | | | | | | | | (EDIT: for mutual fixpoints)
| | | | | * | | | Using a more explicit algebraic type for evars of kind "MatchingVar".Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | A priori considered to be a good programming style.
| | * | | | | | | 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.
| * / | | | | | Fixing #5523 (missing support for complex constructions in recursive notations).Gravatar Hugo Herbelin2017-05-31
| |/ / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We get rid of a complex function doing both an incremental comparison and an effect on names (Notation_ops.compare_glob_constr). For the effect on names, it was actually already done at the time of turning glob_constr to notation_constr, so it could be skipped here. For the comparison, we rely on a new incremental variant of Glob_ops.glob_eq_constr (thanks to Gaëtan for getting rid of the artificial recursivity in mk_glob_constr_eq). Seizing the opportunity to get rid of catch-all clauses in pattern-matching (as advocated by Maxime). Also make indentation closer to the one of other functions.
* / / / / / / 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).
| * / / / / Pretyping cleanup: remove constr_of_global callsGravatar Matthieu Sozeau2017-05-29
|/ / / / /
| | * | | Merge PR#546: Fix for bug #4499 and other minor related bugsGravatar Maxime Dénès2017-05-29
| | |\ \ \
* | | \ \ \ 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#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
|\ \ \ \ \ \ \ \
| | * | | | | | | [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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 17:32:33 +0000