diff options
| author | Pierre-Marie Pédrot | 2016-11-26 16:18:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:44 +0100 |
| commit | b4b90c5d2e8c413e1981c456c933f35679386f09 (patch) | |
| tree | fc84ec244390beb2f495b024620af2e130ad5852 /interp/constrintern.ml | |
| parent | 78a8d59b39dfcb07b94721fdcfd9241d404905d2 (diff) | |
Definining EConstr-based contexts.
This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index e5dd6a6ec3..41e2e4e6ff 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2083,6 +2083,7 @@ let intern_context global_level env impl_env binders = user_err ~loc ~hdr:"internalize" (explain_internalization_error e) let interp_rawcontext_evars env evdref k bl = + let open EConstr in let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> @@ -2093,7 +2094,6 @@ let interp_rawcontext_evars env evdref k bl = let t = understand_tcc_evars env evdref ~expected_type:IsType t' in match b with None -> - let t = EConstr.Unsafe.to_constr t in let d = LocalAssum (na,t) in let impls = if k == Implicit then @@ -2104,8 +2104,6 @@ let interp_rawcontext_evars env evdref k bl = (push_rel d env, d::params, succ n, impls) | Some b -> let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in - let t = EConstr.Unsafe.to_constr t in - let c = EConstr.Unsafe.to_constr c in let d = LocalDef (na, c, t) in (push_rel d env, d::params, n, impls)) (env,[],k+1,[]) (List.rev bl) |