| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-08-26 | Make evarconv and unification able to handle eta for records in presence | Matthieu Sozeau | |
| of metas/evars | |||
| 2014-08-26 | Fix compilation error due to commented code in previous commit by Hugo. | Matthieu Sozeau | |
| 2014-08-25 | Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible | Matthieu Sozeau | |
| to match on a primitive projection application c.(p) using "?f _", binding f to (fun x => x.(p)) with the correct typing. | |||
| 2014-08-25 | Fixing the essence of naming bug #3204: use same strategy for naming | Hugo Herbelin | |
| cases pattern variables than for naming forall/fun binders (but still avoiding constructor names). Note in passing: such as it is implemented, the general strategy is in O(n²) in the number of nested binders, because, when computing the name for each 'fun x => c" (or forall, or a pattern name), the names from the outside c and visibly occurring in c are computed. | |||
| 2014-08-25 | instanciation is French, instantiation is English | Jason Gross | |
| 2014-08-25 | Grammar: "avoiding to" isn't proper, either | Jason Gross | |
| 2014-08-22 | Move UnsatisfiableConstraints to a pretype error. | Matthieu Sozeau | |
| 2014-08-18 | Fixing unification of subterms identified by patterns. | Hugo Herbelin | |
| 2014-08-18 | Refine patch for behavior of unify_to_subterm to allow backtracking on | Matthieu Sozeau | |
| unsatisfiable constraint failures but give sensible error messages if an occurrence was found and only typeclass resolution failed. Fixes MathClasses. | |||
| 2014-08-14 | Remove confusing behavior of unify_with_subterm that could fail with | Matthieu Sozeau | |
| NoOccurenceFound when only typeclass resolution failed. Might break some scripts relying on backtracking on typeclass resolution failures to find other terms to rewrite, which can be fixed using occurrences or directly setoid_rewrite. | |||
| 2014-08-14 | Fix non-printing of coercions for primitive projections (fixes bug #3433). | Matthieu Sozeau | |
| 2014-08-14 | Restrict eta-conversion to inductive records, fixing bug #3310. | Matthieu Sozeau | |
| 2014-08-13 | Bettre pretty-printing of evar maps, avoids printing universe information | Matthieu Sozeau | |
| for typeclass errors. | |||
| 2014-08-10 | Fix bug introduced by earlier commit on first-order unification of primitive | Matthieu Sozeau | |
| projections and their expansion, allowing unfolding when it fails. Cleanup code in reductionops.ml | |||
| 2014-08-09 | Fix unification which was failing when unifying a primitive projection against | Matthieu Sozeau | |
| its expansion if it could reduce (fixes bug #3480). | |||
| 2014-08-09 | Allow pattern matching on the applied form of projections with primitive | Matthieu Sozeau | |
| applications, solving part of bug #3503. | |||
| 2014-08-09 | Do early occur-check in unification to allow eta to fire (fixes bug #3477) | Matthieu Sozeau | |
| 2014-08-09 | Using the asymmetric merging primitive in Evd. | Pierre-Marie Pédrot | |
| 2014-08-09 | Cleaning up interface of ContextSet. | Pierre-Marie Pédrot | |
| Names and arguments were uniformized, and some functions were redesigned to take their typical use-case into account. | |||
| 2014-08-09 | Tentative performance fix for Evd.merge_uctx. | Pierre-Marie Pédrot | |
| The levels added by the context are in general much fewer than the size of the evarmap, so it is better to add them to the latter rather than doing it the other way around. | |||
| 2014-08-08 | Fix evarconv not applying eta when it used to. Fixes bug#3319. | Matthieu Sozeau | |
| 2014-08-07 | Better structure for Ltac pretyping environments. | Pierre-Marie Pédrot | |
| 2014-08-06 | [uconstr]: use a closure instead of eager substitution. | Arnaud Spiwack | |
| This avoids relying on detyping. As Matthieu Sozeau pointed out to me, [understand∘detyping] has no reason to be the identity. This may create surprising behaviour some times (when a detyped term loses its relations to the current context, in particular in terms of universes), and downright incompatibilities in the case of refine. As a bonus this should be a faster implementation of [uconstr] with a leaner memory profile. | |||
| 2014-08-05 | Small code simplification. | Pierre-Marie Pédrot | |
| 2014-08-05 | A new step in the new "standard" naming policy for propositional hypotheses | Hugo Herbelin | |
| obtained from case analysis or induction. Made it under experimental status. This replaces commit bf7d2a3ad2535e7d57db79c17c81aaf67d956965 which was acting at the level of logic.ml. Now acting in tactics.ml. Parts of things to be done about naming (not related to Propositions): induction on H:nat+bool produces hypotheses n and b but destruct on H produces a and b. This is because induction takes the dependent scheme whose names are statically inferred to be a and b while destruct dynamically builds a new scheme. | |||
| 2014-08-03 | - Fix handling of opaque polymorphic definitions which were turned transparent. | Matthieu Sozeau | |
| - Decomment code in reductionops forgotten after debugging. | |||
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ↵ | Matthieu Sozeau | |
| variables. Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's. Abstraction by variables is handled mostly inside the kernel but could be moved outside. | |||
| 2014-08-03 | - Fix has_undefined_evars not using its or_sorts argument anymore. | Matthieu Sozeau | |
| - Allow apply's unification to use conversion even if some polymorphic constants appear in the goal (consistent with occur_meta_or_evar, and evarconv in general). | |||
| 2014-08-01 | Continuing (incomplete) cleaning of Inductiveops. | Hugo Herbelin | |
| 2014-08-01 | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin | |
| - realargs: refers either to the indices of an inductive, or to the proper args of a constructor - params: refers to parameters (which are common to inductive and constructors) - allargs = params + realargs - realdecls: refers to the defining context of indices or proper args of a constructor (it includes letins) - paramdecls: refers to the defining context of params (it includes letins) - alldecls = paramdecls + realdecls | |||
| 2014-07-31 | Add an option to solve typeclass goals generated by apply which can't be | Matthieu Sozeau | |
| catched otherwise due to the discrepancy between evars and metas. | |||
| 2014-07-30 | Avoid introducing additional universes when doing pruning in evarsolve. | Matthieu Sozeau | |
| 2014-07-29 | Rework code for refolding projections in whd_state/whd_simpl to allow Arguments | Matthieu Sozeau | |
| Specifications indicating that the record object must be a constructor. Fixes bug #3432. | |||
| 2014-07-29 | Fix bug #3453, not recognizing primitive projections in Coercion declarations. | Matthieu Sozeau | |
| 2014-07-20 | Use kernel conversion on terms that contain universe variables during ↵ | Matthieu Sozeau | |
| unification, speeding it up considerably Revert backwards-incompatible commit 77df7b1283940d979d3e14893d151bc544f41410 | |||
| 2014-07-17 | Fix coercion code to disallow using cumulativity in the domain of products, ↵ | Matthieu Sozeau | |
| which results in strange changes in user provided terms. | |||
| 2014-07-14 | Add interface function to replace new_Type () | Matthieu Sozeau | |
| 2014-07-10 | Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo). | Matthieu Sozeau | |
| 2014-07-09 | Revert patch making the oracle be used for the transparent state in evarconv, | Matthieu Sozeau | |
| which made CoRN (and probably Ergo) fail. Another option should be found for making a constant not unfoldable by tactics/refinement. | |||
| 2014-07-07 | In flex-flex cases, the undefinedness of an evar can not be preseved after ↵ | Matthieu Sozeau | |
| converting the stacks. Take care of this by recalling unification. | |||
| 2014-07-07 | Missing check of evar instantiation, resulting in missing constraints (bug ↵ | Matthieu Sozeau | |
| from MathClasses). | |||
| 2014-07-03 | Cleanup code related to the constraint solving, which sits now outside the | Matthieu Sozeau | |
| kernel in library/universes.ml. | |||
| 2014-07-03 | Fix eta expansion of primitive records (HoTT bug #78), which now fails ↵ | Matthieu Sozeau | |
| cleanly when called on partially applied constructors. Also protect evar_conv from that case. | |||
| 2014-07-03 | When defining a monomorphic Program, do not allow arbitrary instantiations | Matthieu Sozeau | |
| of the universe context in the obligations, it gets gradually fixed globally by each one of them. Fixes bug found in Misc/Overloading. | |||
| 2014-07-02 | Fix a Not_found anomaly raised by solve_evar_evar, we were breaking the | Matthieu Sozeau | |
| invariant that the evar arguments to that function always have to be undefined. | |||
| 2014-07-01 | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau | |
| 2014-06-30 | Clarifying 'No such bound variable' message in apply, as suggested in #2387 | Hugo Herbelin | |
| 2014-06-29 | When building on-the-fly elimination principles, set the predicates universe ↵ | Matthieu Sozeau | |
| variable as algebraic so it can disappear from the proof (it always gets substituted away from the term). This means less spurious universes remaining in proof terms. | |||
| 2014-06-29 | Really honor the [simpl never] flag in whd_simpl, it was still doing ↵ | Matthieu Sozeau | |
| reductions in case the constant was hiding a direct match for example. Also avoid two lookups of ReductionBehavior per constant application in simpl. | |||
| 2014-06-28 | Quick fix of bug #2996 continued (case of inductive types). | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |