From cad44fcfe8a129af24d4d9d1f86c8be123707744 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 28 Jun 2014 17:13:22 +0200
Subject: Quickly fixing bug #2996: typing functions now check when referring
 to a global reference that the current (goal) env contains all the section
 variables that the global reference expects to be present.

Note that the test for inclusion might be costly: everytime a
conversion happens in a section variable copied in a goal, this
conversion has to be redone when referring to a constant dependent on
this section variable.

It is unclear to me whether we should not instead give global names to
section variables so that they exist even if they are not listed in
the context of the current goal.

Here are two examples which are still problematic:
Section A.
Let B := True : Type.
Definition C := eq_refl : B = True.
Theorem D : Type.
clearbody B.
set (x := C).
unfold C in x.
(* inconsistent context *)

or

Section A.
Let B : Type.
exact True.
Qed.
Definition C := eq_refl : B = True.  (* Note that this violated the Qed. *)
Theorem D : Type.
set (x := C).
unfold C in x.
(* inconsistent context *)
---
 kernel/typeops.mli | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index e6fdf3d6cb..ad0634e6c7 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -120,6 +120,12 @@ val type_of_constant_type_knowing_parameters :
 val type_of_constant_knowing_parameters :
   env -> pconstant -> types Lazy.t array -> types constrained
 
+val type_of_constant_knowing_parameters_in :
+  env -> pconstant -> types Lazy.t array -> types
+
 (** Make a type polymorphic if an arity *)
 val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment ->
   constant_type
+
+(** Check that hyps are included in env and fails with error otherwise *)
+val check_hyps_inclusion : env -> constr -> section_context -> unit
-- 
cgit v1.2.3