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 | |
| 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.
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 4 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
3 files changed, 5 insertions, 5 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 diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 6e46d3625..71da59c49 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -215,7 +215,7 @@ VERNAC COMMAND EXTEND NewFunctionalScheme | (_,fun_name,_)::_ -> begin begin - make_graph (Nametab.global fun_name) + make_graph (Smartlocate.global_with_alias fun_name) end ; try Functional_principles_types.build_scheme fas @@ -245,7 +245,7 @@ END (***** debug only ***) VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY -["Generate" "graph" "for" reference(c)] -> [ make_graph (Nametab.global c) ] +["Generate" "graph" "for" reference(c)] -> [ make_graph (Smartlocate.global_with_alias c) ] END diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 0d254c9af..72613624b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1266,7 +1266,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp let hook _ _ = let opacity = let na_ref = Libnames.Ident (Loc.ghost,na) in - let na_global = Nametab.global na_ref in + let na_global = Smartlocate.global_with_alias na_ref in match na_global with ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant") |