aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/functional_principles_types.ml
Commit message (Expand)AuthorAge
* Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
* Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\
* | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
|/
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\
| * Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
* | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | Removing some goal unsafeness in inductive schemes.Gravatar Pierre-Marie Pédrot2015-10-29
|/
* 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
* Do not pause globing in funind. (Fix bug #4382)Gravatar Guillaume Melquiond2015-10-28
* Univs: fix evar_map leaks bugs in FunctionGravatar Matthieu Sozeau2015-10-02
* 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
* Function now supports puniveresGravatar jforest2015-04-14
* Correcting a bug introduced by universes polymorphismGravatar jforest2015-03-25
* correcting a bug with aliased when using Functional SchemeGravatar forest2015-03-25
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Fixing Functional Induction when applied to an alias (reference manualGravatar Hugo Herbelin2014-11-07
* 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
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofGravatar Pierre-Marie Pédrot2014-06-08
* Enforce a correct exception handling in declaration_hooksGravatar Enrico Tassi2014-06-08
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* - Fix abstract forgetting about new constraints.Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
* Factoring(continued).Gravatar Arnaud Spiwack2013-12-04
* The tactic [admit] exits with the "unsafe" status.Gravatar aspiwack2013-11-02
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* declaration_hooks use EphemeronGravatar gareuselesinge2013-10-18
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 14:44:14 +0000