aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Simplifying an instantiation function using subst_of_rel_context_instance.Gravatar Hugo Herbelin2015-12-05
|
* About building of substitutions from instances.Gravatar Hugo Herbelin2015-12-05
| | | | | | | | | | Redefining adjust_subst_to_rel_context from instantiate_context who was hidden in inductiveops.ml, renamed the latter into subst_of_rel_context_instance and moving them to Vars. The new name highlights that the input is an instance (as for applist) and the output a substitution (as for substl). This is a clearer unified interface, centralizing the difficult de-Bruijn job in one place. It saves a couple of List.rev.
* Experimenting documentation of the Vars.subst functions.Gravatar Hugo Herbelin2015-12-05
| | | | | | | | | | | | | | | | Related questions: - What balance to find between precision and conciseness? - What convention to follow for typesetting the different components of the documentation is unclear? New tentative type substl to emphasize that substitutions (for substl) are represented the other way round compared to instances for application (applist), though there are represented the same way (i.e. most recent/dependent component on top) as instances of evars (mkEvar). Also removing unused subst*_named_decl functions (at least substnl_named_decl is somehow non-sense).
* Contracting one extra beta-redex on the fly when typing branches of "match".Gravatar Hugo Herbelin2015-12-05
|
* A few renaming and simplification in inductive.ml.Gravatar Hugo Herbelin2015-12-05
|
* Experimenting removing strong normalization of the mid-statement in tactic cut.Gravatar Hugo Herbelin2015-12-05
|
* Moving three related small half-general half-ad-hoc utility functionsGravatar Hugo Herbelin2015-12-05
| | | | | next to each other, waiting for possible integration into a more uniform API.
* An example in centralizing similar functions to a common place so thatGravatar Hugo Herbelin2015-12-05
| | | | | cleaning the interfaces is eventually easier. Here, adding find_mrectype_vect to simplify vnorm.ml.
* Using x in output test-suite Cases.v (cosmetic).Gravatar Hugo Herbelin2015-12-05
|
* Ensuring that documentation of mli code works in the presence of utf-8Gravatar Hugo Herbelin2015-12-05
| | | | characters.
* Getting rid of some quoted tactics in Tauto.Gravatar Pierre-Marie Pédrot2015-12-05
|
* Specializing the Dyn module to each usecase.Gravatar Pierre-Marie Pédrot2015-12-04
| | | | | | Actually, we never mix the various uses of each dynamic type created through the Dyn module. To enforce this statically, we functorize the Dyn module so that we recover a fresh instance at each use point.
* Getting rid of the dynamic node of the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-04
|
* Removing the last use of valueIn in Tauto.Gravatar Pierre-Marie Pédrot2015-12-04
|
* Removing dynamic inclusion of constrs in tactic AST.Gravatar Pierre-Marie Pédrot2015-12-04
|
* Getting rid of dynamic hacks in Setoid_newring.Gravatar Pierre-Marie Pédrot2015-12-04
|
* Removing the globTacticIn primitive.Gravatar Pierre-Marie Pédrot2015-12-03
| | | | | It was not used in Coq codebase, and the only known user was ssreflect up to commit 95354e0dee.
* Fixing Tauto compilation for older versions of OCaml.Gravatar Pierre-Marie Pédrot2015-12-03
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\
* | Removing the last use of tacticIn in setoid_ring.Gravatar Pierre-Marie Pédrot2015-12-03
| |
* | Removing the use of tacticIn in Tauto.Gravatar Pierre-Marie Pédrot2015-12-03
| |
| * Adding a target report to test-suite's Makefile to get a short summary.Gravatar Hugo Herbelin2015-12-02
| |
| * Slight simplification of code for pat/constr.Gravatar Hugo Herbelin2015-12-02
| |
| * Improving syntax of pat/constr introduction pattern so thatGravatar Hugo Herbelin2015-12-02
| | | | | | | | | | | | pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat. Open to other suggestions of syntax though.
| * Dead code from August 2014 in apply in.Gravatar Hugo Herbelin2015-12-02
| |
| * Update history of revisions.Gravatar Hugo Herbelin2015-12-02
| |
| * Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Gravatar Hugo Herbelin2015-12-02
| |
| * Univs/Program: update the universe context with global universeGravatar Matthieu Sozeau2015-12-02
| | | | | | | | | | constraints at the time of Next Obligation/Solve Obligations so that interleaving definitions and obligation solving commands works properly.
| * Fix bug #4444: Next Obligation performed after a Section opening wasGravatar Matthieu Sozeau2015-12-02
| | | | | | | | | | | | | | using the wrong context. This is very bad style but currently unavoidable, at least we don't throw an anomaly anymore.
| * Add an option to deactivate compatibility printing of primitiveGravatar Matthieu Sozeau2015-12-02
| | | | | | | | projections (off by default).
| * Fix a bug in externalisation which prevented printing of projectionsGravatar Matthieu Sozeau2015-12-02
| | | | | | | | using dot notation.
* | Removing dead code in Obligations.Gravatar Pierre-Marie Pédrot2015-12-02
| |
* | New algorithm for universe cycle detections.Gravatar Jacques-Henri Jourdan2015-12-01
| |
* | Remove unneeded fixpoint in normalize_context_set. Note that it is noGravatar Matthieu Sozeau2015-12-01
| | | | | | | | | | | | longer stable w.r.t. equality constraints as the universe graph will choose different canonical levels depending on the equalities given to it (l = r vs r = l).
| * vio: fix argument parsing (progress on #4442)Gravatar Enrico Tassi2015-12-01
| |
* | Simplify coqdep lexer by removing global references.Gravatar Guillaume Melquiond2015-11-30
| |
| * Test for bug #4149.Gravatar Pierre-Marie Pédrot2015-11-30
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-29
|\|
| * Test-suite files for closed bugsGravatar Matthieu Sozeau2015-11-28
| |
| * Closed bugs.Gravatar Matthieu Sozeau2015-11-28
| |
| * Univs: correctly register universe binders for lemmas.Gravatar Matthieu Sozeau2015-11-28
| |
| * Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
| | | | | | | | | | | | | | | | | | Prop levels. As they are typed assuming all variables are >= Set now, and this was breaking an invariant in typing. Only one instance in the standard library was used in Hurkens, which can be avoided easily. This also avoids displaying unnecessary >= Set constraints everywhere.
| * Avoid recording spurious Set <= Top.i constraints which are alwaysGravatar Matthieu Sozeau2015-11-27
| | | | | | | | valid (when Top.i is global and hence > Set).
| * Fix [Polymorphic Hint Rewrite].Gravatar Matthieu Sozeau2015-11-27
| |
| * Fixing the "parsing rules with idents later declared as keywords" problem.Gravatar Hugo Herbelin2015-11-26
| | | | | | | | | | | | | | The fix was actually elementary. The lexer comes with a function to compare parsed tokens against tokens of the parsing rules. It is enough to have this function considering an ident in a parsing rule to be equal to the corresponding string parsed as a keyword.
| * Make the pretty printer resilient to incomplete nametab (progress on #4363).Gravatar Enrico Tassi2015-11-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | The nametab in which the error message is printed is not the one in which the error message happens. This reveals a weakness in the fix_exn code: the fix_exn function should be pure, while in some cases (like this one) uses the global state (the nametab) to print a term in a pretty way (the shortest non-ambiguous name for constants). This patch makes the externalization phase (used by term printing) resilient to an incomplete nametab, so that printing a term in the wrong nametab does not mask the original error.
| * Adding the Printing Projections options to the index.Gravatar Pierre-Marie Pédrot2015-11-26
| |
* | More efficient implementation of equality-up-to-universes in Universes.Gravatar Pierre-Marie Pédrot2015-11-26
| | | | | | | | | | | | Instead of accumulating constraints which are not present in the original graph, we parametrize the equality function by a function actually merging those constraints in the current graph. This prevents doing the work twice.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-26
|\|
* | More invariants in UState.Gravatar Pierre-Marie Pédrot2015-11-26
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-28 00:24:37 +0000