aboutsummaryrefslogtreecommitdiff
path: root/test-suite/modules
AgeCommit message (Expand)Author
2020-05-30Remove info tactic, deprecated in 8.5Jim Fehrle
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
2018-11-27Fix #9076 (warning appears when running test suite)Maxime Dénès
2018-10-04Test-suite: avoid explicit references to “Top”Vincent Laporte
2018-10-04test-suite: cleaningVincent Laporte
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2018-03-05CHANGES and tests for with Definition @{univs}Gaëtan Gilbert
2018-02-21Merge PR #6740: Adding a sanity check on inductive variance subtyping.Maxime Dénès
2018-02-16Adding a test for the construction that was broken in Coccinelle.Pierre-Marie Pédrot
2018-02-15Adding a test for variance subtyping in the module system.Pierre-Marie Pédrot
2017-10-19Moving bug numbers to BZ# format in the test-suite.Théo Zimmermann
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-07-11Properly handling polymorphic inductive subtyping in the kernel.Pierre-Marie Pédrot
2017-07-11Cleaning up the implementation of module subtyping in the kernel.Pierre-Marie Pédrot
2013-01-18Unset Asymmetric Patternspboutill
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2011-03-05Starting being more explicit on the reasons why module subtyping fails.herbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2007-05-25git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9859 85f007b7-540e-04...soubiran
2007-02-21Removed some useless code in mod_typing that was redundant with safe_typing.soubiran
2007-01-19Prise en compte des univers algébriques dans les types inférés dansherbelin
2007-01-17Correction bug #1302herbelin
2006-12-22remplacement d'un test d'egalite par un test de convertibilite dans injection...jforest
2006-10-17Clarification des contraintes sur le contexte de paramètres desherbelin
2006-10-05Correction de deux cas où les types inductifs n'étaient pas comparésherbelin
2006-09-14Correction du bug #1181jforest
2006-05-10Conformité nouveaux principes: Declare Module non utilisable pour définir u...herbelin
2006-04-15Test synchronisation chargement objets non logiquesherbelin
2005-12-21Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
2005-12-21MAJ syntaxe v7 avant activation en syntaxe v8herbelin
2005-12-21Anciennement déplacé dans 'output'herbelin
2003-11-28Simplest Demo on modulescoq
2003-09-22L'exemple phare de modules - simplifie pour TPHOLscoq
2003-05-05Corrige Bug (PR#290)coq
2003-02-06commentairecoq
2003-01-31MAJ syntaxe modules + nouveau fichier mod_decl qui explique toutcoq
2002-11-24Remplacement de Syntactic Definition par Notationherbelin
2002-09-27Encore quelques rangements dans Nametab + petits trucscoq
2002-08-16Encore quelques tests sur modules...coq
2002-08-13Petites corrections ici et lacoq
2002-08-02Modules dans COQ\!\!\!\!coq
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:42:18 +0000