aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2014-10-26Applying like-first selection for destruct in hypotheses.Hugo Herbelin
2014-10-26Fixing destruct/induction with a using clause on a non-inductive type,Hugo Herbelin
2014-10-26Dead code + typo.Hugo Herbelin
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-24Change reduction_of_red_expr to return an e_reduction_function returningMatthieu Sozeau
2014-10-24Fixing order of hypothesis in goal hypotheses compaction for coqtop.Hugo Herbelin
2014-10-23Fixing order of declarations in the function which compacts variablesHugo Herbelin
2014-10-22Pushing Pierre's factorization of names in goal context printing fromHugo Herbelin
2014-10-22Removing an unused variant of Context.fold_named_context_reverse.Hugo Herbelin
2014-10-22Fix missing lift in VM and native compiler (second part of #2729).Maxime Dénès
2014-10-22Fixing an evar leak in pattern-matching compilation (#3758).Hugo Herbelin
2014-10-22Add more primitives to the [Monad.Make] arguments.Arnaud Spiwack
2014-10-21Porting Hugo's fix 98f3abb83a to native compiler.Maxime Dénès
2014-10-21Dead code.Hugo Herbelin
2014-10-20Fixing a (new) part of bug #2729.Hugo Herbelin
2014-10-20A patch for printing "match" when constructors are defined with let-inHugo Herbelin
2014-10-20Fixing a bug in the presence of let-in in inductive arity.Hugo Herbelin
2014-10-17When facing problem ?id = ?id' in resolution of return predicate,Hugo Herbelin
2014-10-17New experimental heuristic printing strategy for evar instances: WeHugo Herbelin
2014-10-17Re-displaying evar instances in debugger.Hugo Herbelin
2014-10-16Refine: proper scoping of the future goals.Arnaud Spiwack
2014-10-16Move the handling of the principal evar from refine to evd.Arnaud Spiwack
2014-10-16Move the handling a new evars from the [Proofview.Refine] module to [Evd].Arnaud Spiwack
2014-10-16Evd: a few comments to document the increasingly wide internal [evar_map] type.Arnaud Spiwack
2014-10-16Evd: remove/update obsolete comments.Arnaud Spiwack
2014-10-15To stay closer to non-primitive projections, only unfold primitiveMatthieu Sozeau
2014-10-15Make use of unfolded primitive projections when elaborating match on aMatthieu Sozeau
2014-10-15Fix bug 3637.Matthieu Sozeau
2014-10-15Reenable FO unification of primitive projections and their eta-expandedMatthieu Sozeau
2014-10-15Modify the heuristic for unfolding lhs or rhs in evarconv, consideringMatthieu Sozeau
2014-10-15Implement a different strategy to expand primitive projections only whenMatthieu Sozeau
2014-10-15Add an option to not print primitive projection parameters, which canMatthieu Sozeau
2014-10-14Oops, forgot a fix needed after the rebase.Matthieu Sozeau
2014-10-14Fix bug #3698: stack overflow due to eta+canonical structures inMatthieu Sozeau
2014-10-13Adding a tactic which fails if one of the goals under focus is dependent in a...Hugo Herbelin
2014-10-13Moving function about locs in locusops.Hugo Herbelin
2014-10-13English typo in a function name of evarconv.Hugo Herbelin
2014-10-13Added support for several impossible cases in compilation of "match".Hugo Herbelin
2014-10-12Tentative fix for a badly used Option.get in Reductionops.Pierre-Marie Pédrot
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-10-10Do not expand primitive projections eagerly in evarconv, but onlyMatthieu Sozeau
2014-10-10Add debug printers for projections, fix printing of evar constraintsMatthieu Sozeau
2014-10-10Add a "Debug Tactic Unification" option and correct the first-orderMatthieu Sozeau
2014-10-10Make constrMatching and detyping more robust with respect toMatthieu Sozeau
2014-10-10Fix bug due to shadowing a variable name in tacredMatthieu Sozeau
2014-10-08fix make mlidocPierre Boutillier
2014-10-08Fixing the anomaly in bug #3045 (a filter was not type-safe inHugo Herbelin
2014-10-07Build unfolded versions of the primitive projection in let (a, p) := ...Matthieu Sozeau
2014-10-07Avoid a warning with Meta's names in debugger.Hugo Herbelin
2014-10-05A few improvements on pattern-matching compilation.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 16:12:12 +0000