aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/inductiveops.ml
Commit message (Expand)AuthorAge
* Replace Typeops by Fast_typeopsGravatar Gaetan Gilbert2016-12-12
* 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
* Fix reopened bug #3317.Gravatar Matthieu Sozeau2016-07-06
* Disallow dependent case on prim records w/o etaGravatar Matthieu Sozeau2016-07-06
* Renaming to more generic has_dependent_elim testGravatar Matthieu Sozeau2016-07-06
* Move is_prim... to Inductiveops and correct SchemeGravatar Matthieu Sozeau2016-07-06
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
| * Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | Fixing e7f7fc3e058 (wrong chop on contexts). This fixes test-suite.Gravatar Hugo Herbelin2015-12-15
* | | Unifying betazeta_applist and prod_applist into a clearer interface.Gravatar Hugo Herbelin2015-12-05
* | | Simplifying an instantiation function using subst_of_rel_context_instance.Gravatar Hugo Herbelin2015-12-05
* | | About building of substitutions from instances.Gravatar Hugo Herbelin2015-12-05
* | | An example in centralizing similar functions to a common place so thatGravatar Hugo Herbelin2015-12-05
|/ /
* | Univs: bug fix.Gravatar Matthieu Sozeau2015-07-07
* | Fix handling of primitive projections in VM.Gravatar Maxime Dénès2015-07-05
| * Add a flag to deactivate guard checking in the kernel.Gravatar Arnaud Spiwack2015-06-26
|/
* Fully fixing bug #3491 (anomaly when building _rect scheme in theGravatar Hugo Herbelin2015-03-25
* Add support so that the type of a match in an inductive type with let-inGravatar Hugo Herbelin2015-02-27
* Fixing typo resulting in wrong printing of return clauses forGravatar Hugo Herbelin2015-02-27
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* Fix non-printing of coercions for primitive projections (fixes bug #3433).Gravatar Matthieu Sozeau2014-08-14
* A new step in the new "standard" naming policy for propositional hypothesesGravatar Hugo Herbelin2014-08-05
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* Continuing (incomplete) cleaning of Inductiveops.Gravatar Hugo Herbelin2014-08-01
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Cleanup code related to the constraint solving, which sits now outside theGravatar Matthieu Sozeau2014-07-03
* Quick fix of bug #2996 continued (case of inductive types).Gravatar Hugo Herbelin2014-06-28
* Deactivate the "Standard Propositions Naming" flag, source of a lot ofGravatar Hugo Herbelin2014-06-26
* Fix type_of_inductive_knowing_conclusion, relying on an actually broken univ_...Gravatar Matthieu Sozeau2014-06-25
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* Use of "H"-based names for propositional hypotheses obtained byGravatar Hugo Herbelin2014-06-01
* Reuse universe level substitutions for template polymorphism, fixing performanceGravatar Matthieu Sozeau2014-05-09
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-19 07:37:47 +0000