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