aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/implicit.v
AgeCommit message (Collapse)Author
2020-02-13Arguments: removing the restriction to set an anonymous parameter implicit.Hugo Herbelin
This was already possible manually using "{ _ }" in the type of declaration. This was also possible for type classes. So, no reason to forbid in Arguments.
2020-02-04Correct bug in non max local implicit argumentsSimonBoulier
+ tests in the test-suite for non max local implicit arguments
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2019-12-04Manual implicit arguments: more robustness tests.Hugo Herbelin
- Warn in some places where {x:T} is not assumed to occur (e.g. in argument of an application, or of a match). - Warn when an implicit argument occurs several times with the same name. - Accept local anonymous {_:T} with explicitation possible using name `arg_k`. We obtain this by using a flag (impl_binder_index) which tells if we are in a position where implicit arguments matter and, if yes, the index of the next binder.
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2012-06-12Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15431 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-18Fixed a Not_found bug when declaring in a section some implicitherbelin
arguments for a constant not defined in the section. Also fixed some typos in the doc of implicit arguments in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14816 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-02-08Correct handling of existential variables when multiple differentmsozeau
instances of the lemma are rewritten at once. Cleanup dead code and put the problematic cases in the test-suite. Also fix some test-suite scripts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13813 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-12-03Fixing bug using explictly declared implicit arguments in inductive arities.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13671 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-05Export definition of type implicits_list for contribs + fixed aherbelin
discharge bug of implicit arguments related to commit 13484 (multiple implicit arguments sequences patch). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13500 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-04Fixing bugs in previous commits about implicit arguments:herbelin
- fixing r13483 (supposed dead code in impargs was actually half-living: implicit arguments mode should merge with the {...} manually given implicit arguments but not with the "Implicit Arguments [...]" arguments), - fixing code of drop_first_implicits in r13484. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13490 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-10-03Added multiple implicit arguments rules per name.herbelin
Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]". This should a priori be used with care (it might be a bit disturbing seeing the same constant used with apparently incompatible signatures). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-29Revision 12439 continued, printing part (notations to names behaveherbelin
like the name they refer to). Fixing buggy test-suite implicit.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12442 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-26Local/Global revision 12418 continuedherbelin
- Fixing non-export of newly created Local Argument Scope. - Fixing bad discharge of local variables in nested sections (bug still exists in v8.2). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12420 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-16Correction bug calcul des implicites en présence d'evars dans les typesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9827 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Extension et réorganisation de l'interprétation des (co-)points fixesherbelin
- Relâchement de l'exigence que les types des paramètres et le type des (co-)points fixes soient donnés. Ils peuvent maintenant être inférés à partir des autres informations de types. - Plus de déclaration séparée de celles des fonctions d'un bloc de points fixes qui n'interviennent pas dans la définition des autres (collect_non_rec): remplacement par un simple warning en cas de non dépendance mutuelle de toutes les fonctions du bloc (de toutes façons les fonctions qui intervenaient dans les autres sans en dépendre - càd les fonctions définissables avant la partie point fixe - n'étaient pas détectées) - Ajout du test de dépendance mutuel au cas des co-points fixes Extension et réorganisation de l'interprétation des blocs de définitions (co-)inductives: relâchement de l'exigence que les types des paramètres soient donnés. Ils peuvent maintenant être inférés à partir des autres informations des blocs d'inductifs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9108 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-12Correctionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5463 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28Exemple de Fredericherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5399 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13Niveau V8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4894 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13Fermeture de la section maintenant necessaireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4893 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-21Ajout d'un exemple de Christineherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2365 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2297 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:19:49 +0000