Fix bug 2307

Evars of source "ImpossibleCase" that remain undefined at the end of
case analysis are now defined to ID (forall A : Type, A -> A).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13023 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 29 insertions, 27 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1a30b4e2c..ad55cf4f7 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -63,27 +63,6 @@ let error_wrong_predicate_arity_loc loc env c n1 n2 =
 let error_needs_inversion env x t =
   raise (PatternMatchingError (env, NeedsInversion (x,t)))
 
-(**********************************************************************)
-(* Functions to deal with impossible cases *)
-
-let impossible_default_case = ref None
-
-let set_impossible_default_clause c = impossible_default_case := Some c
-
-let coq_unit_judge =
-  let na1 = Name (id_of_string "A") in
-  let na2 = Name (id_of_string "H") in
-  fun () ->
-    match !impossible_default_case with
-    | Some (id,type_of_id) ->
-	make_judge id type_of_id
-    | None ->
-	(* In case the constants id/ID are not defined *)
-	make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1)))
-                 (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2)))
-
-(**********************************************************************)
-
 module type S = sig
   val compile_cases :
     loc -> case_style ->
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index ab1f409ca..cc064bc4d 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -45,8 +45,6 @@ val error_wrong_predicate_arity_loc : loc -> env -> constr -> constr -> constr -
 
 val error_needs_inversion : env -> constr -> types -> 'a
 
-val set_impossible_default_clause : constr * types -> unit
-
 (** {6 Compilation primitive. } *)
 type alias_constr =
   | DepAlias
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index ad4e70089..486fd05b3 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -548,11 +548,15 @@ let apply_conversion_problem_heuristic env evd pbty t1 t2 =
 
 let consider_remaining_unif_problems env evd =
   let (evd,pbs) = extract_all_conv_pbs evd in
-  List.fold_left
+  let heuristic_solved_evd = List.fold_left
     (fun evd (pbty,env,t1,t2) ->
       let evd', b = apply_conversion_problem_heuristic env evd pbty t1 t2 in
 	if b then evd' else Pretype_errors.error_cannot_unify env evd (t1, t2))
-    evd pbs
+    evd pbs in
+    Evd.fold_undefined (fun ev ev_info evd' -> match ev_info.evar_source with
+			  |_,ImpossibleCase -> 
+			     Evd.define ev (j_type (coq_unit_judge ())) evd'
+			  |_ -> evd') heuristic_solved_evd heuristic_solved_evd
 
 (* Main entry points *)
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 1c0bf2fbc..c099504f6 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -966,3 +966,21 @@ let context_chop k ctx =
     | (_, []) -> anomaly "context_chop"
   in chop_aux [] (k,ctx)
 
+(*******************************************)
+(* Functions to deal with impossible cases *)
+(*******************************************)
+let impossible_default_case = ref None
+
+let set_impossible_default_clause c = impossible_default_case := Some c
+
+let coq_unit_judge =
+  let na1 = Name (id_of_string "A") in
+  let na2 = Name (id_of_string "H") in
+  fun () ->
+    match !impossible_default_case with
+    | Some (id,type_of_id) ->
+	make_judge id type_of_id
+    | None ->
+	(* In case the constants id/ID are not defined *)
+	make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1)))
+                 (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2)))
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 5a0ba3cab..5d99b24de 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -61,8 +61,7 @@ val it_mkNamedLambda_or_LetIn : init:constr -> named_context -> constr
 val it_named_context_quantifier :
   (named_declaration -> 'a -> 'a) -> init:'a -> named_context -> 'a
 
-(*********************************************************************
-   Generic iterators on constr                                        *)
+(** {6 Generic iterators on constr} *)
 
 val map_constr_with_named_binders :
   (name -> 'a -> 'a) ->
@@ -248,3 +247,7 @@ val has_polymorphic_type : constant -> bool
 val on_judgment       : (types -> types) -> unsafe_judgment -> unsafe_judgment
 val on_judgment_value : (types -> types) -> unsafe_judgment -> unsafe_judgment
 val on_judgment_type  : (types -> types) -> unsafe_judgment -> unsafe_judgment
+
+(** {6 Functions to deal with impossible cases } *)
+val set_impossible_default_clause : constr * types -> unit
+val coq_unit_judge : unit -> unsafe_judgment