diff options
| author | Enrico Tassi | 2019-01-07 17:38:00 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-01-07 17:38:00 +0100 |
| commit | cd0b6e930d8753f68f5ed84ddcf00be09cd38990 (patch) | |
| tree | eee1305ee0129c47deb76f521b6f9b7a3aef9be1 /pretyping | |
| parent | ffcb5526d33c1eaa2016dd3af9e3dffd932b7874 (diff) | |
| parent | 759e049e8322c90e9cb9b511167d06e49f81818e (diff) | |
Merge PR #9241: Fix #9240: Register for IDProp causes anomaly when non constant
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e6e1530e36..ed28cc7725 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -46,15 +46,10 @@ let () = Goptions.(declare_bool_option { (* Functions to deal with impossible cases *) (*******************************************) let impossible_default_case env = - let type_of_id = - let open Names.GlobRef in - match Coqlib.lib_ref "core.IDProp.type" with - | ConstRef c -> c - | VarRef _ | IndRef _ | ConstructRef _ -> assert false - in + let type_of_id = Coqlib.lib_ref "core.IDProp.type" in let c, ctx = UnivGen.fresh_global_instance env (Coqlib.(lib_ref "core.IDProp.idProp")) in - let (_, u) = Constr.destConst c in - Some (c, Constr.mkConstU (type_of_id, u), ctx) + let (_, u) = Constr.destRef c in + Some (c, Constr.mkRef (type_of_id, u), ctx) let coq_unit_judge = let open Environ in |