aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
Commit message (Expand)AuthorAge
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Univs: fix bug #4375, accept universe binders on (co)-fixpointsGravatar Matthieu Sozeau2015-10-28
* Do not pause globing in funind. (Fix bug #4382)Gravatar Guillaume Melquiond2015-10-28
* Partly fixes #3225. Removed some old experimental stuff in funind.Gravatar Pierre Courtieu2015-10-19
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Univs: fix after rebase (from_ctx/from_env)Gravatar Matthieu Sozeau2015-10-02
* Univs: fix evar_map leaks bugs in FunctionGravatar Matthieu Sozeau2015-10-02
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Remove dirty debug printing from funind.Gravatar Maxime Dénès2015-04-15
* Function now supports puniveresGravatar jforest2015-04-14
* better debug in recdefGravatar jforest2015-04-14
* correction of a bug reported by Tristan CrolardGravatar jforest2015-04-13
* Fix #3590 for good this time, by changing the API, change's argument nowGravatar Matthieu Sozeau2015-04-10
* Correcting a bug introduced by universes polymorphismGravatar jforest2015-03-25
* correcting a bug with aliased when using Functional SchemeGravatar forest2015-03-25
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* handling Functional Scheme for required but not imported modulesGravatar Julien Forest2014-12-11
* Closing bug 3837Gravatar Julien Forest2014-12-08
* Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Gravatar Hugo Herbelin2014-12-07
* Writing Tactics.keep in the new monad.Gravatar Pierre-Marie Pédrot2014-11-21
* Fixing side bug in db37c9f3f32ae7 delaying interpretation of theGravatar Hugo Herbelin2014-11-16
* Fixing Functional Induction when applied to an alias (reference manualGravatar Hugo Herbelin2014-11-07
* Removing the legacy intro tactic code.Gravatar Pierre-Marie Pédrot2014-11-07
* Writing rename_hyps in the new monad.Gravatar Pierre-Marie Pédrot2014-11-03
* Don't raise an error when printing intro-patterns in [functional induction].Gravatar Arnaud Spiwack2014-11-01
* 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
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Correction of error message (bug 3359)Gravatar Julien Forest2014-09-22
* Fixing bug 3951Gravatar Julien Forest2014-09-22
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 09:59:13 +0000