aboutsummaryrefslogtreecommitdiff
path: root/pretyping/inductiveops.mli
AgeCommit message (Expand)Author
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Fix bugsAmin Timany
2017-06-16Subtyping inference for inductoves and recordsAmin Timany
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-02-14Namegen primitives now apply on evar constrs.Pierre-Marie Pédrot
2017-02-14Eliminating parts of the right-hand side compatibility layerPierre-Marie Pédrot
2017-02-14Leminv API using EConstr.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Cases API using EConstr.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2016-07-06Disallow dependent case on prim records w/o etaMatthieu Sozeau
2016-07-06Renaming to more generic has_dependent_elim testMatthieu Sozeau
2016-07-06Move is_prim... to Inductiveops and correct SchemeMatthieu Sozeau
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-05An example in centralizing similar functions to a common place so thatHugo Herbelin
2015-07-05Fix handling of primitive projections in VM.Maxime Dénès
2015-03-25Fully fixing bug #3491 (anomaly when building _rect scheme in theHugo Herbelin
2015-01-12Update headers.Maxime Dénès
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-08-14Fix non-printing of coercions for primitive projections (fixes bug #3433).Matthieu Sozeau
2014-08-05A new step in the new "standard" naming policy for propositional hypothesesHugo Herbelin
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-08-01Continuing (incomplete) cleaning of Inductiveops.Hugo Herbelin
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-06-01Use of "H"-based names for propositional hypotheses obtained byHugo Herbelin
2014-05-31Dead code + typo.Hugo Herbelin
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2012-08-08Updating headers.herbelin
2012-03-02"Let in" in pattern hell, one more iterationpboutill
2012-01-16Inductiveops.nb_*{,_env} cleaningpboutill
2011-12-18Granted legitimate wish #2607 (not exposing crude fixpoint body ofherbelin
2011-04-06A few extra combinators about rel_declaration/named_declaration + a bit of docherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-13- Inductive types in the "using" option of auto/eauto/firstorder areherbelin
2009-08-11Ensures that let-in's in arities of inductive types work well. Maybe notherbelin
2009-07-15- Fixing bug #2139 (kernel-based test of well-formation of eliminationherbelin
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 07:16:10 +0000