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/g_indfun.ml4 | |
| 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/g_indfun.ml4')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
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 |