aboutsummaryrefslogtreecommitdiff
path: root/toplevel/indschemes.ml
AgeCommit message (Expand)Author
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
2017-02-01Merge branch 'v8.6'Pierre-Marie Pédrot
2017-01-23Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-12-23Excluding explicitly coinductive types in Scheme Equality (#5284).Hugo Herbelin
2016-12-22Fixing anomaly EqUnknown in Equality Scheme (#5278).Hugo Herbelin
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-02Fix bug #5069: Scheme Equality gives anomalies in sections.Pierre-Marie Pédrot
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-07-06Renaming to more generic has_dependent_elim testMatthieu Sozeau
2016-07-06Move is_prim... to Inductiveops and correct SchemeMatthieu Sozeau
2016-07-06primproj: warning and avoid error.Matthieu Sozeau
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-18Reuse the typing_flags datatype for inductives.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-03-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-07Adding backtraces to scheme error messages.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-11-20Univs: generation of induction schemes should not generated uselessMatthieu Sozeau
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-10-02Univs: fix environment handling in scheme building.Matthieu Sozeau
2015-09-23Hopefully better names to constructors of internal_flag, as discussedHugo Herbelin
2015-07-27Improving over 26aa224293 in reporting unexpected error during scheme creation.Hugo Herbelin
2015-07-27Fixing bug #3736 (anomaly instead of error/warning/silence onHugo Herbelin
2015-06-24Add corresponding field in `VernacInductive`.Arnaud Spiwack
2015-01-24Equality Schemes options: reverting commit ff9f94634 which isHugo Herbelin
2015-01-12Update headers.Maxime Dénès
2014-09-16better error messageEnrico Tassi
2014-09-04Type definitions with [Variant] don't generate inductive schemes by default.Arnaud Spiwack
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-08-30Simplify even further the declaration of primitive projections,Matthieu Sozeau
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-07-01Making code and doc agree on "Set Equality Schemes" (see also bug #2550).Hugo Herbelin
2014-06-17Safer entry point of primitive projections in the kernel, now it does recognizeMatthieu Sozeau
2014-05-06- Fix RecTutorial, and mutual induction schemes getting the wrong names.Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Rework handling of universes on top of the STM, allowing for delayedMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-23cList: a few alternative to hashtbl-based uniquize, distinct, subsetletouzey
2013-08-08State Transaction Machinegareuselesinge
2013-05-08Uniformizing the [if_warn] flag used for warning printing and putppedrot
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 19:49:35 +0000