diff options
| author | letouzey | 2012-05-29 11:09:15 +0000 |
|---|---|---|
| committer | letouzey | 2012-05-29 11:09:15 +0000 |
| commit | 6d961ac24305f26e896b602bdabe0e9c3c7cbf05 (patch) | |
| tree | dadc934c94e026149da2ae08144af769f4e9cb6c /plugins/decl_mode/decl_interp.ml | |
| parent | 255f7938cf92216bc134099c50bd8258044be644 (diff) | |
global_reference migrated from Libnames to new Globnames, less deps in grammar.cma
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/decl_mode/decl_interp.ml')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 7c097c6d69..6d3a5be392 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -157,7 +157,7 @@ let special_whd env = let infos=Closure.create_clos_infos Closure.betadeltaiota env in (fun t -> Closure.whd_val infos (Closure.inject t)) -let _eq = Libnames.constr_of_global (Coqlib.glob_eq) +let _eq = Globnames.constr_of_global (Coqlib.glob_eq) let decompose_eq env id = let typ = Environ.named_type id env in @@ -247,7 +247,7 @@ let rec glob_of_pat = add_params (pred n) (GHole(dummy_loc, Evar_kinds.TomatchTypeParameter(ind,n))::q) in let args = List.map glob_of_pat lpat in - glob_app(loc,GRef(dummy_loc,Libnames.ConstructRef cstr), + glob_app(loc,GRef(dummy_loc,Globnames.ConstructRef cstr), add_params mind.Declarations.mind_nparams args) let prod_one_hyp = function @@ -334,7 +334,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = (if expected = 0 then str "none" else int expected) ++ spc () ++ str "expected.") in let app_ind = - let rind = GRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in + let rind = GRef (dummy_loc,Globnames.IndRef pinfo.per_ind) in let rparams = List.map detype_ground pinfo.per_params in let rparams_rec = List.map |