aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Gravatar Maxime Dénès2018-02-28
|\
* \ Merge PR #6823: Fixes #6821 (bug in protecting notation printing from ↵Gravatar Maxime Dénès2018-02-28
|\ \ | | | | | | | | | infinite eta-expansion)
* \ \ Merge PR #6812: Rename release_lexer_state to the more descriptive ↵Gravatar Maxime Dénès2018-02-28
|\ \ \ | | | | | | | | | | | | get_lexer_state.
* \ \ \ Merge PR #6752: Remove from CircleCI builds that are already taken care of ↵Gravatar Maxime Dénès2018-02-28
|\ \ \ \ | | | | | | | | | | | | | | | by Travis.
* \ \ \ \ Merge PR #6543: Update headers and creditsGravatar Maxime Dénès2018-02-24
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6784: New IR in VM: ClambdaGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6819: Document Arguments extra scopes flagGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6803: coqdev.el: add space at the end of compile-commandGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6599: Decimals in preludeGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6745: [ast] Improve precision of Ast location recognition in ↵Gravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | serialization.
| | | | | | * | | | | | New IR in VM: Clambda.Gravatar Maxime Dénès2018-02-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This intermediate representation serves two purposes: 1- It is a preliminary step for primitive machine integers, as iterators will be compiled to Clambda. 2- It makes the VM compilation passes closer to the ones of native_compute. Once we unifiy the representation of values, we should be able to factorize the lambda-code generation between the two compilers, as well as the reification code. This code was written by Benjamin Grégoire and myself.
| | | | | | * | | | | | Fix map iterator on nativelambda.Gravatar Maxime Dénès2018-02-23
| | | | | | | | | | | |
| | | | | | | | | | * | Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).Gravatar Hugo Herbelin2018-02-23
| |_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | More precisely when matching "f t" with "(fun ?x => .. ((fun ?x' => ?y) ?z') ..) ?z" do not allow expansion of f since otherwise, we recursively have to match "f t" with the same pattern.
| | | | | * | | | | | Document Arguments extra scopes flagGravatar Jasper Hugunin2018-02-22
| |_|_|_|/ / / / / / |/| | | | | | | | |
| | | | | | | | * | Tweak developer documentation.Gravatar Jim Fehrle2018-02-22
| | | | | | | | | |
| | | | | | | | * | Rename release_lexer_state to the more descriptive get_lexer_state.Gravatar Jim Fehrle2018-02-22
| | | | | | |_|/ / | | | | | |/| | |
| * | | | / | | | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
|/ / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
| | | | | | * / Remove from CircleCI builds that are already taken care of by Travis.Gravatar Théo Zimmermann2018-02-21
| |_|_|_|_|/ / |/| | | | | |
* | | | | | | Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_predGravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6767: [ci] add elpiGravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6283: A pre-commit hook to magically fix whitespace issues.Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6748: Fix bug #6529: nf_evar_info to nf the evars' env not just ↵Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | the concl
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6740: Adding a sanity check on inductive variance subtyping.Gravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | |
| | | | | | | | | | | * | Update CREDITS.Gravatar Théo Zimmermann2018-02-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In particular, add a mention of SSReflect.
| | | | | | | | | | | * | More accurate and complete headers.Gravatar Théo Zimmermann2018-02-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Remove the mention of specific labs (irrelevant for a copyright notice). Add a mention to represent other contributors and a pointer to CREDITS.
| | | | | | | | | | | * | Mention the CREDITS file in CONTRIBUTING.Gravatar Théo Zimmermann2018-02-21
| | | | | | | | | | | | |
| | | | | | | | | | | * | Remove redundant COPYRIGHT file.Gravatar Théo Zimmermann2018-02-21
| |_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This information is already present in CREDITS.
| | | | | | | | | * | | coqdev.el: add space at the end of compile-commandGravatar Gaëtan Gilbert2018-02-21
| |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | That way you can just type [-j] instead of having to remember to add a space yourself.
| | | | | | | | * | | Add CHANGES entry for decimals in preludeGravatar Jason Gross2018-02-20
| | | | | | | | | | |
| | | | | | | | * | | Update SearchPattern.out for numeral notationsGravatar Jason Gross2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There is more churn than there should be because SearchPattern uses a non-local sorting algorithm; the comparison function considers many constants equal in priority and leaves it up to the heap structure to break ties, which seems wrong. This has been reported as [bug #5573](https://coq.inria.fr/bugs/show_bug.cgi?id=5573).
| | | | | | | | * | | Doc: add Decimal-related files to index-list.html.templateGravatar Jason Gross2018-02-20
| | | | | | | | | | |
| | | | | | | | * | | Decimal goodies : conversion to/from Coq stringsGravatar Pierre Letouzey2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Just because it's fun and easy. Not used by the Numeral Notation command.
| | | | | | | | * | | Decimal: proofs that conversions from/to nat,N,Z are bijectionsGravatar Pierre Letouzey2018-02-20
| | | | | | | | | | |
| | | | | | | | * | | Decimal: simple representation of base-10 numbersGravatar Pierre Letouzey2018-02-20
| |_|_|_|_|_|_|/ / / |/| | | | | | | | |
| | | | | | | | * | Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Hugo Herbelin2018-02-20
| |_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Computation of the sort of the inductive type was done before ensuring that the arguments of the inductive type had the correct types, possibly brutally failing with `NotArity` in case one of the types expected to be typed with an arity was not so.
| | | | * | | | | Adding a test for wish #5532.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | |
| | | | * | | | | Documenting use of primitive entry names for restricting syntax in notations.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | |
| | | | * | | | | Extended documentation for notations referring to binders.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Talking about the difference between ident and pattern. Giving examples.
| | | | * | | | | Trying a hack to support {'pat|P} without breaking compatibility.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Concretely, we bypass the following limitation: The notation "{ ' pat | P }" broke the parsing of expressions of the form "{ forall x, P } + { Q }". Indeed the latter works thanks to a tolerance of Camlp5 in parsing "forall x, P" at level 200 while the rule asks to actually parse the interior of "{ ... }" at level 99 (the reason for 99 is to be below the rule for "M : T" which is at level 100, so that "{ x : A | P }" does not see "x : A" as a cast). Adding an extra "'"; pat = pattern in parallel to c = constr LEVEL "99" broke the tolerance for constr at level 200. We fix this by adding an ad hoc rule for "{ binder_constr }" in the native grammar (g_constr.ml4). Actually, this is inconsistent with having a rule for "{ constr at level 99 }" in Notations.v. We should have both rules in Notations.v or both rules hard-wired in the native grammar. But I still don't know what is the best decision to take, so leaving as it at the current time. Advantages of hard-wiring both rules in g_constr.ml4: a bit simpler in metasyntax.ml (no need to ensure that the rule exist). Disadvantages: if one wants a different initial state without the business needing the "{ }" for sumbool, sumor, sig, sigT, one still have the rules there. Advantages of having them in Notations.v: more modular, we can change the initial state. Disadvantages: one would need a new kind of modifier, something like "x at level 99 || binder_constr", with all the difficulty to find a nice, intuitive, name for "binder_constr", and the difficulty of understanding if there is a generality to this "||" disjunction operator, and whether it should be documented or not.
| | | | * | | | | Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | |
| | | | * | | | | Change default for notations with variables bound to both terms and binders.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For compatibility, the default is to parse as ident and not as pattern.
| | | | * | | | | Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Concretely, we provide "constr as ident", "constr as strict pattern" and "constr as pattern". This tells to parse a binder as a constr, restricting to only ident or to only a strict pattern, or to a pattern which can also be an ident. The "strict pattern" modifier allows to restrict the use of patterns in printing rules. This allows e.g. to select the appropriate rule for printing between {x|P} and {'pat|P}.
| | | | * | | | | Notations: A step in cleaning constr_entry_key.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Avoid dummy use of unit - Do not decide as early as parsing the default level for pattern - Prepare to further extensions
| | | | * | | | | Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Renaming it register_grammars_by_name.
| | | | * | | | | More flexibility in locating or referring to a notation.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We generalize the possibility to refer to a notation not only by its "_ U _" form but also using its "a 'U' b". (Wish from EJGA)
| | | | * | | | | More structured printing in unicode notations for binders.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | |
| | | | * | | | | Being more flexible on format Adding a warning to be more informativeGravatar Hugo Herbelin2018-02-20
| | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 03:26:23 +0000