| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-01-22 | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction. | Maxime Dénès | |
| 2018-01-22 | Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints. | Maxime Dénès | |
| 2018-01-19 | Add test-suite file for issue #6617. | Cyprien Mangin | |
| 2018-01-18 | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder. | Maxime Dénès | |
| 2018-01-17 | Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop) | Maxime Dénès | |
| 2018-01-17 | Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction | Jasper Hugunin | |
| 2018-01-17 | Use let-in aware prod_applist_assum in dtauto and firstorder. | Jasper Hugunin | |
| Fixes #6490. `prod_applist_assum` is copied from `kernel/term.ml` to `engine/termops.ml`, and adjusted to work with econstr. This change uncovered a bug in `Hipattern.match_with_nodep_ind`, where `has_nodep_prod_after` counts both products and let-ins, but was only being passed `mib.mind_nparams`, which does not count let-ins. Replaced with (Context.Rel.length mib.mind_params_ctxt). | |||
| 2017-12-18 | Merge PR #6436: Fix #5368: Canonical structure unification fails. | Maxime Dénès | |
| 2017-12-15 | Fix #5368: Canonical structure unification fails. | Pierre-Marie Pédrot | |
| Universe instances were lost during constructions of the canonical instance. | |||
| 2017-12-14 | Add tactics to reset and display the Ltac profile | Jason Gross | |
| This is useful for tactics that run a bunch of tests and need to display the profile for each of them. | |||
| 2017-12-14 | Merge PR #6386: Catch errors while coercing 'and' intro patterns | Maxime Dénès | |
| 2017-12-11 | Allow LtacProf tactics to be called | Jason Gross | |
| This fixes #6378. Previously the ML module was never declared anywhere. Thanks to @cmangin for the pointer. | |||
| 2017-12-11 | Catch errors while coercing 'and' intro patterns | Tej Chajed | |
| Fixes GH#6384 and GH#6385. | |||
| 2017-12-06 | Fix #6323: stronger restrict universe context vs abstract. | Gaëtan Gilbert | |
| In the test we do [let X : Type@{i} := Set in ...] with Set abstracted. The constraint [Set < i] was lost in the abstract. Universes of a monomorphic reference [c] are considered to appear in the term [c]. | |||
| 2017-12-01 | Fix #6297: handle constraints like (u+1 <= Set/Prop) | Gaëtan Gilbert | |
| 2017-12-01 | Proper nametab handling of global universe names | Matthieu Sozeau | |
| They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced | |||
| 2017-11-30 | Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ↵ | Maxime Dénès | |
| #3125) | |||
| 2017-11-28 | In injection/inversion, consider all template-polymorphic types as injectable. | Hugo Herbelin | |
| In particular singleton inductive types are considered injectable, even in the absence of the option "Set Keep Proof Equalities". This fixes #3125 (and #4560, #6273). | |||
| 2017-11-28 | Fix (partial) #4878: option to stop autodeclaring axiom as instance. | Gaëtan Gilbert | |
| 2017-11-25 | Fix #5347: unify declaration of axioms with and without bound univs. | Gaëtan Gilbert | |
| Note that this makes the following syntax valid: Axiom foo@{i} bar : Type@{i}. (ie putting a universe declaration on the first axiom in the list, the declaration then holds for the whole list). | |||
| 2017-11-25 | Make restrict_universe_context stronger. | Gaëtan Gilbert | |
| This fixes BZ#5717. Also add a test and fix a changed test. | |||
| 2017-11-24 | Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRing | Maxime Dénès | |
| 2017-11-24 | Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion | Maxime Dénès | |
| 2017-11-23 | Merge PR #6203: Fix universe polymorphic Program obligations. | Maxime Dénès | |
| 2017-11-23 | Recognizing Z in romega up to conversion. | Hugo Herbelin | |
| 2017-11-23 | Using is_conv rather than eq_constr to find `nat` or `Z` in omega. | Hugo Herbelin | |
| Moving at the same to a passing "env sigma" style rather than passing "gl". Not that it is strictly necessary, but since we had to move functions taking only a "sigma" to functions taking also a "env", we eventually adopted the "env sigma" style. (The "gl" style would have been as good.) This answers wish #4717. | |||
| 2017-11-23 | Fixing a 8.7 regression of ring_simplify in ArithRing. | Hugo Herbelin | |
| With help from Guillaume (see discussion at https://github.com/coq/coq/issues/6191). | |||
| 2017-11-23 | Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag. | Maxime Dénès | |
| 2017-11-22 | Fix universe polymorphic Program obligations. | Matthieu Sozeau | |
| The universes of the obligations should all be non-algebraic as they might appear in instances of other obligations and instances only take non-algebraic universes as arguments. | |||
| 2017-11-20 | Merge PR #6166: Fix regression in treating Defined as defined | Maxime Dénès | |
| 2017-11-20 | Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 ↵ | Maxime Dénès | |
| (clause "where" with implicit arguments) | |||
| 2017-11-20 | Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵ | Maxime Dénès | |
| unbound rel | |||
| 2017-11-19 | Fix #5790: make Hint Resolve <- respect univ polymorphism flag. | Gaëtan Gilbert | |
| 2017-11-15 | Fix regression in treating Defined as defined | Tej Chajed | |
| Fixes #6165. | |||
| 2017-11-15 | Fix #5761: cbv on undefined evars under binders produces unbound rel | Gaëtan Gilbert | |
| When an evar is undefined we need to substitute inside the evar instance. With help from @herbelin and @psteckler to identify the issue from a large test case. | |||
| 2017-11-14 | Fixes #6129 (declaration of coercions made compatible with local definitions). | Hugo Herbelin | |
| 2017-11-14 | One more step in fixing #5762 ("where" clause). | Hugo Herbelin | |
| We improve one step further the heuristics to sort out if a variable is a notation variable or a named variable. This allows to support the following which was still failing. Reserved Notation "# x" (at level 0). Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I). We rely here on the property that a binding variable of same name as a notation variables is itself considered bound by the notation. This becomes however to be a bit tricky for sorting out if the variable has to be output to the glob file or not. | |||
| 2017-11-13 | Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac. | Maxime Dénès | |
| 2017-11-06 | Merge PR #6074: Refining PR#924 (insensitivity of projection heuristics to ↵ | Maxime Dénès | |
| alphabet). | |||
| 2017-11-06 | Merge PR #1139: Add a linter. | Maxime Dénès | |
| 2017-11-05 | Refining PR#924 (insensitivity of projection heuristics to alphabet). | Hugo Herbelin | |
| We refine the criterion for selecting a projection. Before PR#924 it was alphabetic (i.e. morally "random" up to alpha-conversion). After PR#924 it was chronological. We refine a bit more by giving priority to simple projections when they exist over projections which include an evar instantiation (and which may actually be ill-typed). | |||
| 2017-11-04 | Adding support for syntax "let _ := e in e'" in Ltac. | Hugo Herbelin | |
| Adding a file fixing #5996 and which uses this feature. | |||
| 2017-11-03 | Merge PR #6047: A generic printer for ltac values | Maxime Dénès | |
| 2017-11-03 | Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous ↵ | Maxime Dénès | |
| variables). | |||
| 2017-11-03 | Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition). | Maxime Dénès | |
| 2017-11-02 | Binding ltac printing functions to the system of generic printing. | Hugo Herbelin | |
| This concerns pr_value and message_of_value. This has a few consequences. For instance, no more ad hoc message "a term" or "a tactic", when not enough information is available for printing, one gets a generic message "a value of type foobar". But we also have more printers, satisfying e.g. request #5786. | |||
| 2017-10-30 | Fixing #2881 ("change with" failing in an Ltac definition). | Hugo Herbelin | |
| We fix by interpreting the pattern in "change pat with term" in strict mode by using the same interning code as for "match goal" (even if the pattern is dropped afterwards). | |||
| 2017-10-28 | Fixing #5401 (printing of patterns with bound anonymous variables). | Hugo Herbelin | |
| This fixes also #5731, #6035, #5364. | |||
| 2017-10-27 | Merge PR #677: Trunk+abstracting injection flags | Maxime Dénès | |
| 2017-10-26 | Passing around the flag for injection so that tactics calling inj at | Hugo Herbelin | |
| ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |