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

7 files changed, 33 insertions, 28 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 6cfe1421f7..8a4bc63650 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -135,7 +135,7 @@ let make_con dir id = Libnames.encode_con dir id
 let id = make_con datatypes_module (id_of_string "id")
 let type_of_id = make_con datatypes_module (id_of_string "ID")
 
-let _ = Cases.set_impossible_default_clause (mkConst id,mkConst type_of_id)
+let _ = Termops.set_impossible_default_clause (mkConst id,mkConst type_of_id)
 
 (** Natural numbers *)
 let nat_kn = make_kn datatypes_module (id_of_string "nat")
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1a30b4e2cf..ad55cf4f72 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 ab1f409ca4..cc064bc4da 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 ad4e700897..486fd05b3d 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 1c0bf2fbcf..c099504f6f 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 5a0ba3cab5..5d99b24de2 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
diff --git a/test-suite/bugs/closed/shouldsucceed/2307.v b/test-suite/bugs/closed/shouldsucceed/2307.v
new file mode 100644
index 0000000000..7c04949539
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2307.v
@@ -0,0 +1,3 @@
+Inductive V: nat -> Type := VS n: V (S n).
+Definition f (e: V 1): nat := match e with VS 0 => 3 end.
+