aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/inductiveops.mli
Commit message (Expand)AuthorAge
* 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
* Use of "H"-based names for propositional hypotheses obtained byGravatar Hugo Herbelin2014-06-01
* Dead code + typo.Gravatar Hugo Herbelin2014-05-31
* 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
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Updating headers.Gravatar herbelin2012-08-08
* "Let in" in pattern hell, one more iterationGravatar pboutill2012-03-02
* Inductiveops.nb_*{,_env} cleaningGravatar pboutill2012-01-16
* Granted legitimate wish #2607 (not exposing crude fixpoint body ofGravatar herbelin2011-12-18
* A few extra combinators about rel_declaration/named_declaration + a bit of docGravatar herbelin2011-04-06
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Inductive types in the "using" option of auto/eauto/firstorder areGravatar herbelin2009-09-13
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* - Fixing bug #2139 (kernel-based test of well-formation of eliminationGravatar herbelin2009-07-15
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* fixing r11433 again:Gravatar barras2008-10-07
* Correction d'une incohérence de typage des inductifs polymorphes: lesGravatar herbelin2008-07-25
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
* Ajout allowed_sortsGravatar herbelin2006-10-01
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* - Distinction explicite des parties paramètres et arguments dans le typeGravatar herbelin2006-04-27
* Fonctions retournant les arits des constructeurs et inductifsGravatar herbelin2006-01-30
* Moving subst_inductive from tacinterp to inductiveops for better for reuse in...Gravatar herbelin2005-02-18
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* Deplacement des fonctions de typage des predicate de Cases a la V7 de inducti...Gravatar herbelin2004-08-24
* Nouvelle en-têteGravatar herbelin2004-07-16
* Ajout mis_constructor_nargs_envGravatar herbelin2003-11-18
* correction (temporaire ?) d'un probleme de Printer.prterm_env utilisant quand...Gravatar letouzey2002-12-13
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Ajout map_inductive_type et map_ind_familyGravatar herbelin2002-06-13
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* petit nettoyage de kernel/inductiveGravatar barras2002-02-07
* Ajout make_arity_signatureGravatar herbelin2001-11-20
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05