aboutsummaryrefslogtreecommitdiff
path: root/pretyping/indrec.mli
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-04-10Remove calls to global env from indrecMaxime Dénès
2018-09-28Functionalizing calls to the environment in Himsg.Hugo Herbelin
2018-06-13[vernac] Add option to force building really mutual induction schemesMatthieu Sozeau
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
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
2015-10-29Removing some goal unsafeness in inductive schemes.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
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-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-11-09- Fixed bug 1968 (inversion failing due to a Not_found bug introduced inherbelin
2007-05-17Nettoyage et standardisation des messages d'erreurs.herbelin
2005-12-17Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...herbelin
2005-11-02Types inductifs parametriquesmohring
2004-07-16Nouvelle en-têteherbelin
2003-09-12Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...herbelin
2003-09-09Ajout construction If primitive dans constr_expr et rawconstrherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-11-05GROS COMMIT:barras
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:08:36 +0000