aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2014-11-04Experimentally applying eager evar substitution at the same time asHugo Herbelin
2014-11-03Fixing confused code for interpretations of evar instances.Hugo Herbelin
2014-11-03Fixing inefficiency in typeclass resolution.Pierre-Marie Pédrot
2014-11-02Fixing subterm matched for destruct when it is matched from prefix.Hugo Herbelin
2014-11-02Cosmetic changes.Hugo Herbelin
2014-11-02Fixing 1177da327 (reorganization of the test for generic selection ofHugo Herbelin
2014-10-31Reorganization of the test for generic selection of occurrences inHugo Herbelin
2014-10-31Enlarge the cases where the like first selection is used in destruct.Hugo Herbelin
2014-10-27Removing dead code from Evd.Pierre-Marie Pédrot
2014-10-27Removing the Evd.diff function.Pierre-Marie Pédrot
2014-10-27Removing the Evd.merge function.Pierre-Marie Pédrot
2014-10-27Dead codeHugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-18 11:01:40 +0000