diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 22:50:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 15:59:10 +0200 |
| commit | c51fb2fae0e196012de47203b8a71c61720d6c5c (patch) | |
| tree | e49c2d38b6c841dc6514944750d21ed08ab94bce /plugins/funind/indfun.ml | |
| parent | 437063a0c745094c5693d1c5abba46ce375d69c6 (diff) | |
[api] Deprecate GlobRef constructors.
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 48e3129599..99efe3e5e2 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -8,7 +8,6 @@ open EConstr open Pp open Indfun_common open Libnames -open Globnames open Glob_term open Declarations open Tactypes @@ -59,7 +58,7 @@ let functional_induction with_clean c princl pat = let princ,g' = (* then we get the principle *) try let g',princ = - Tacmach.pf_eapply (Evd.fresh_global) g (Globnames.ConstRef (Option.get princ_option )) in + Tacmach.pf_eapply (Evd.fresh_global) g (GlobRef.ConstRef (Option.get princ_option )) in princ,g' with Option.IsNone -> (*i If there is not default lemma defined then, @@ -836,7 +835,7 @@ let make_graph (f_ref : GlobRef.t) = let sigma = Evd.from_env env in let c,c_body = match f_ref with - | ConstRef c -> + | GlobRef.ConstRef c -> begin try c,Global.lookup_constant c with Not_found -> raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) ) |