diff options
| author | Hugo Herbelin | 2017-04-13 20:29:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-31 01:04:28 +0200 |
| commit | 4865160fa1f2e9ce03b37b9cb3ac99c35e9c4e4d (patch) | |
| tree | 16c0005afb7bbf78fdae33166b67c3c81c56364e /interp | |
| parent | bcc9165aec1a80d563d7060ef127ad022e9ed008 (diff) | |
Renaming interp_rawcontext_evars using a more "standard" name.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4dcf287efc..1d5d8e8658 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2071,7 +2071,7 @@ let intern_context global_level env impl_env binders = with InternalizationError (loc,e) -> user_err ?loc ~hdr:"internalize" (explain_internalization_error e) -let interp_rawcontext_evars env evdref k bl = +let interp_glob_context_evars env evdref k bl = let open EConstr in let (env, par, _, impls) = List.fold_left @@ -2100,6 +2100,6 @@ let interp_rawcontext_evars env evdref k bl = let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params = let int_env,bl = intern_context global_level env impl_env params in - let x = interp_rawcontext_evars env evdref shift bl in + let x = interp_glob_context_evars env evdref shift bl in int_env, x |