diff options
| -rw-r--r-- | interp/coqlib.ml | 2 | ||||
| -rw-r--r-- | pretyping/cases.ml | 21 | ||||
| -rw-r--r-- | pretyping/cases.mli | 2 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 8 | ||||
| -rw-r--r-- | pretyping/termops.ml | 18 | ||||
| -rw-r--r-- | pretyping/termops.mli | 7 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2307.v | 3 |
7 files changed, 33 insertions, 28 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 6cfe1421f..8a4bc6365 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 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 diff --git a/test-suite/bugs/closed/shouldsucceed/2307.v b/test-suite/bugs/closed/shouldsucceed/2307.v new file mode 100644 index 000000000..7c0494953 --- /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. + |