diff options
| author | Matthieu Sozeau | 2013-12-13 16:39:44 +0000 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:57 +0200 |
| commit | 29794b8acf407518716f8c02c2ed20729f8802e5 (patch) | |
| tree | a7952e066c733ed10af5a5f43fcbff3ab960971d /plugins | |
| parent | 55e62174683f293c8f966d8bd486fcb511f66221 (diff) | |
- Fix abstract forgetting about new constraints.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 3 |
2 files changed, 3 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 05cdd288c1..8a9c7d2e7b 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -645,7 +645,7 @@ let build_case_scheme fa = (* Constrintern.global_reference id *) (* in *) let funs = (fun (_,f,_) -> - try Universes.unsafe_constr_of_global (Nametab.global f) + try fst (Universes.unsafe_constr_of_global (Nametab.global f)) with Not_found -> Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in let first_fun,u = destConst funs in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 50e7507f4d..8496bbbb35 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -75,7 +75,8 @@ let type_of_const t = Const sp -> Typeops.type_of_constant (Global.env()) sp |_ -> assert false -let constr_of_global = Universes.unsafe_constr_of_global +let constr_of_global x = + fst (Universes.unsafe_constr_of_global x) let constant sl s = constr_of_global (find_reference sl s) |