aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* 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
* A few Global.env removed.Gravatar Hugo Herbelin2014-10-04
* Fixing ennoying warning about evars named ?23 and so on.Gravatar Hugo Herbelin2014-10-03
* Fixing #3623 (unbound evars in types in a call to "change with").Gravatar Hugo Herbelin2014-10-03
* Fixing #3634 (wrong env in "cannot instantiate because not in itsGravatar Hugo Herbelin2014-10-03
* Fixing interpretation of constr under binders which was broken afterGravatar Hugo Herbelin2014-10-02
* Completing fixing order of parameters when translating fromGravatar Hugo Herbelin2014-10-02
* Work around issues with FO unification trying to unify terms ofGravatar Matthieu Sozeau2014-10-02
* Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv.Gravatar Matthieu Sozeau2014-10-02
* Fix cbn behavior wrt simpl no matchGravatar Pierre Boutillier2014-10-01
* Fix the refolding by cbn of mutal constants defined in not included modulesGravatar Pierre Boutillier2014-10-01
* Fixing new failure of #3017 after 012fe1a96ba81ab (Referring to evarsGravatar Hugo Herbelin2014-10-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 12:34:12 +0000