| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-05 | Experimenting removing strong normalization of the mid-statement in tactic cut. | Hugo Herbelin | |
| 2015-12-05 | Moving three related small half-general half-ad-hoc utility functions | Hugo Herbelin | |
| next to each other, waiting for possible integration into a more uniform API. | |||
| 2015-12-05 | An example in centralizing similar functions to a common place so that | Hugo Herbelin | |
| cleaning the interfaces is eventually easier. Here, adding find_mrectype_vect to simplify vnorm.ml. | |||
| 2015-12-05 | Using x in output test-suite Cases.v (cosmetic). | Hugo Herbelin | |
| 2015-12-05 | Ensuring that documentation of mli code works in the presence of utf-8 | Hugo Herbelin | |
| characters. | |||
| 2015-12-05 | Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction) | Hugo Herbelin | |
| based on a suggestion of Guillaume M. (done like this in ssreflect). This is actually consistent with the hack of using "destruct (1)" to mean the term 1 by opposition to the use of "destruct 1" to mean the first non-dependent hypothesis of the goal. | |||
| 2015-12-05 | Fix CHANGES. | Hugo Herbelin | |
| 2015-12-05 | Getting rid of some quoted tactics in Tauto. | Pierre-Marie Pédrot | |
| 2015-12-04 | Specializing the Dyn module to each usecase. | Pierre-Marie Pédrot | |
| 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. | |||
| 2015-12-04 | Getting rid of the dynamic node of the tactic AST. | Pierre-Marie Pédrot | |
| 2015-12-04 | Fix in setoid_rewrite in Type: avoid the generation of a rigid universe | Matthieu Sozeau | |
| on applications of inverse (flip) on a crelation. This was poluting universe constraints of lemmas using generalized rewriting in Type. | |||
| 2015-12-04 | Removing the last use of valueIn in Tauto. | Pierre-Marie Pédrot | |
| 2015-12-04 | Removing dynamic inclusion of constrs in tactic AST. | Pierre-Marie Pédrot | |
| 2015-12-04 | Getting rid of dynamic hacks in Setoid_newring. | Pierre-Marie Pédrot | |
| 2015-12-03 | Removing the globTacticIn primitive. | Pierre-Marie Pédrot | |
| It was not used in Coq codebase, and the only known user was ssreflect up to commit 95354e0dee. | |||
| 2015-12-03 | Fixing Tauto compilation for older versions of OCaml. | Pierre-Marie Pédrot | |
| 2015-12-03 | Univs: fix bug #4443. | Matthieu Sozeau | |
| Do not substitute rigid variables during minimization, keeping their equality constraints instead. | |||
| 2015-12-03 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-03 | Improving over printing of let-tuple (see #4447). | Hugo Herbelin | |
| For instance, #4447 is now printed: λ Ca Da : ℕAlg, let (ℕ, ℕ0) := (Ca, Da) in let (C, p) := ℕ in let (c₀, cs) := p in let (D, p0) := ℕ0 in let (d₀, ds) := p0 in {h : C → D & ((h c₀ = d₀) * (∀ c : C, h (cs c) = ds (h c)))%type} : ℕAlg → ℕAlg → Type | |||
| 2015-12-03 | Removing the last use of tacticIn in setoid_ring. | Pierre-Marie Pédrot | |
| 2015-12-03 | Removing the use of tacticIn in Tauto. | Pierre-Marie Pédrot | |
| 2015-12-02 | Adding a target report to test-suite's Makefile to get a short summary. | Hugo Herbelin | |
| 2015-12-02 | Slight simplification of code for pat/constr. | Hugo Herbelin | |
| 2015-12-02 | Improving syntax of pat/constr introduction pattern so that | Hugo Herbelin | |
| pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat. Open to other suggestions of syntax though. | |||
| 2015-12-02 | Dead code from August 2014 in apply in. | Hugo Herbelin | |
| 2015-12-02 | Update history of revisions. | Hugo Herbelin | |
| 2015-12-02 | Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG. | Hugo Herbelin | |
| 2015-12-02 | Univs/Program: update the universe context with global universe | Matthieu Sozeau | |
| constraints at the time of Next Obligation/Solve Obligations so that interleaving definitions and obligation solving commands works properly. | |||
| 2015-12-02 | Fix bug #4444: Next Obligation performed after a Section opening was | Matthieu Sozeau | |
| using the wrong context. This is very bad style but currently unavoidable, at least we don't throw an anomaly anymore. | |||
| 2015-12-02 | Add an option to deactivate compatibility printing of primitive | Matthieu Sozeau | |
| projections (off by default). | |||
| 2015-12-02 | Fix a bug in externalisation which prevented printing of projections | Matthieu Sozeau | |
| using dot notation. | |||
| 2015-12-02 | Removing dead code in Obligations. | Pierre-Marie Pédrot | |
| 2015-12-01 | New algorithm for universe cycle detections. | Jacques-Henri Jourdan | |
| 2015-12-01 | Remove unneeded fixpoint in normalize_context_set. Note that it is no | Matthieu Sozeau | |
| 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). | |||
| 2015-12-01 | vio: fix argument parsing (progress on #4442) | Enrico Tassi | |
| 2015-11-30 | Simplify coqdep lexer by removing global references. | Guillaume Melquiond | |
| 2015-11-30 | Test for bug #4149. | Pierre-Marie Pédrot | |
| 2015-11-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-28 | Test-suite files for closed bugs | Matthieu Sozeau | |
| 2015-11-28 | Closed bugs. | Matthieu Sozeau | |
| 2015-11-28 | Univs: correctly register universe binders for lemmas. | Matthieu Sozeau | |
| 2015-11-27 | Univs: entirely disallow instantiation of polymorphic constants with | Matthieu Sozeau | |
| 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. | |||
| 2015-11-27 | Avoid recording spurious Set <= Top.i constraints which are always | Matthieu Sozeau | |
| valid (when Top.i is global and hence > Set). | |||
| 2015-11-27 | Fix [Polymorphic Hint Rewrite]. | Matthieu Sozeau | |
| 2015-11-26 | Fixing the "parsing rules with idents later declared as keywords" problem. | Hugo Herbelin | |
| 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. | |||
| 2015-11-26 | Make the pretty printer resilient to incomplete nametab (progress on #4363). | Enrico Tassi | |
| 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. | |||
| 2015-11-26 | Adding the Printing Projections options to the index. | Pierre-Marie Pédrot | |
| 2015-11-26 | More efficient implementation of equality-up-to-universes in Universes. | Pierre-Marie Pédrot | |
| 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. | |||
| 2015-11-26 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-26 | More invariants in UState. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |