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

3 files changed, 49 insertions, 5 deletions

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index d248ba70e5..72095e6c49 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -29,6 +29,15 @@ let meta_type env mv =
 let vect_lift = Array.mapi lift
 let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
 
+let constant_type_knowing_parameters env cst jl =
+  let paramstyp = Array.map (fun j -> j.uj_type) jl in
+  type_of_constant_knowing_parameters env (constant_type env cst) paramstyp
+
+let inductive_type_knowing_parameters env ind jl =
+  let (mib,mip) = lookup_mind_specif env ind in
+  let paramstyp = Array.map (fun j -> j.uj_type) jl in
+  Inductive.type_of_inductive_knowing_parameters env mip paramstyp
+
 (* The typing machine without information, without universes but with
    existential variables. *)
 
@@ -93,12 +102,14 @@ let rec execute env evd cstr =
 	  match kind_of_term f with
 	    | Ind ind ->
 		(* Sort-polymorphism of inductive types *)
-		judge_of_inductive_knowing_parameters env ind
-		  (jv_nf_evar (evars_of evd) jl)
+		make_judge f
+		  (inductive_type_knowing_parameters env ind
+		    (jv_nf_evar (evars_of evd) jl))
 	    | Const cst -> 
 		(* Sort-polymorphism of inductive types *)
-		judge_of_constant_knowing_parameters env cst
-		  (jv_nf_evar (evars_of evd) jl)
+		make_judge f
+		  (constant_type_knowing_parameters env cst
+		    (jv_nf_evar (evars_of evd) jl))
 	    | _ -> 
 		execute env evd f
 	in
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index adb18daa7a..06178324d9 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -102,6 +102,7 @@ let pf_nf_betaiota               = pf_reduce (fun _ _ -> nf_betaiota)
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
 let pf_type_of                   = pf_reduce type_of
+let pf_get_type_of               = pf_reduce Retyping.get_type_of
 
 let pf_conv_x                   = pf_reduce is_conv
 let pf_conv_x_leq               = pf_reduce is_conv_leq
@@ -109,7 +110,7 @@ let pf_const_value              = pf_reduce (fun env _ -> constant_value env)
 let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
 let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
-let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_type_of gls)
+let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls)
 
 let pf_check_type gls c1 c2 = 
   ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2)))
diff --git a/test-suite/success/hyps_inclusion.v b/test-suite/success/hyps_inclusion.v
new file mode 100644
index 0000000000..21bfc0758a
--- /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.