diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-07 21:17:03 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-07 21:24:04 +0100 |
| commit | 2393592c9e5a609e19a96250e2e7588c1aa28ca9 (patch) | |
| tree | d7b9d562e391e2bf0953c50e36e16c5ed3131435 /plugins/funind/functional_principles_types.ml | |
| parent | 269fc07f93f979ae4a71eb6670bcac338f67f455 (diff) | |
Fixing Functional Induction when applied to an alias (reference manual
for Functional Induction was failing because of minus now an alias).
Knowing that minus is an alias for Sub.nat, there are still two bugs in
Functional Induction (Pierre or Julien?):
"Functional Scheme minus_ind := Induction for minus Sort Prop." is
failing when Nat is not imported.
"functional induction (minus n m)" is failing because looking for
sub_ind while the scheme is named minus_ind.
Diffstat (limited to 'plugins/funind/functional_principles_types.ml')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 26706321b..545f8931f 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -597,7 +597,7 @@ let build_scheme fas = (fun (_,f,sort) -> let f_as_constant = try - match Nametab.global f with + match Smartlocate.global_with_alias f with | Globnames.ConstRef c -> c | _ -> Errors.error "Functional Scheme can only be used with functions" with Not_found -> @@ -629,7 +629,7 @@ let build_case_scheme fa = (* Constrintern.global_reference id *) (* in *) let funs = (fun (_,f,_) -> - try fst (Universes.unsafe_constr_of_global (Nametab.global f)) + try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) with Not_found -> Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in let first_fun,u = destConst funs in |