aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-01-22 08:26:30 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-01-22 08:26:30 +0000
commit8f49fb5a04926e28597905bbc052dcecc254eef3 (patch)
tree864ff81faca8002eeaf7e3455bc3f02dc657e676 /test-suite
parentad43624ded04198eee7ce4cc6d8e4c8564967ede (diff)
Correction pour le rapport de bug #1325 par rétablissement du
comportement pré-inductifs polymorphes vis à vis du test d'inclusion des hypothèses de section (i.e. test dans le noyau mais pas dans typing.ml qui est le typeur utilisé généralement par les tactiques). En effet, les variables de section sont vues par les tactiques comme des variables locales qui sont modifiables (p.ex. par conversion). Mais le changement de la signature des variables de section fait échouer le typage noyau (qui exige une égalité syntaxique des types de ces variables) pour les demandes de typage en provenance des tactiques. Quelle est la bonne solution ? - Faut-il comparer les variables de section modulo réduction dans le noyau ? - Faut-il continuer à utiliser un typeur qui ne teste pas les hyps de section pour les tactiques, comme c'était le cas avant les inductifs polymorphes (c'est la solution pragmatique adoptée pour résoudre #1325) - Faut-il éviter la confusion entre variables de section et variables de but ? Incidemment, branchement de Tacmach.hnf_type_of sur Retyping, ce qui, outre des calculs de typage allégés pour les tactiques, évite aussi de tomber sur le comportement du bug #1325. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9510 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/success/hyps_inclusion.v32
1 files changed, 32 insertions, 0 deletions
diff --git a/test-suite/success/hyps_inclusion.v b/test-suite/success/hyps_inclusion.v
new file mode 100644
index 000000000..21bfc0758
--- /dev/null
+++ b/test-suite/success/hyps_inclusion.v
@@ -0,0 +1,32 @@
+(* Simplified example for bug #1325 *)
+
+(* Explanation: the proof engine see section variables as goal
+ variables; especially, it can change their types so that, at
+ type-checking, the section variables are not recognized
+ (Typeops.check_hyps_inclusion raises "types do no match"). It
+ worked before the introduction of polymorphic inductive types because
+ tactics were using Typing.type_of and not Typeops.typing; the former
+ was not checking hyps inclusion so that the discrepancy in the types
+ of section variables seen as goal variables was not a problem (at the
+ end, when the proof is completed, the section variable recovers its
+ original type and all is correct for Typeops) *)
+
+Section A.
+Variable H:not True.
+Lemma f:nat->nat. destruct H. exact I. Defined.
+Goal f 0=f 1.
+red in H.
+(* next tactic was failing wrt bug #1325 because type-checking the goal
+ detected a syntactically different type for the section variable H *)
+case 0.
+Reset A.
+
+(* Variant with polymorphic inductive types for bug #1325 *)
+
+Section A.
+Variable H:not True.
+Inductive I (n:nat) : Type := C : H=H -> I n.
+Goal I 0.
+red in H.
+case 0.
+Reset A.