diff options
Diffstat (limited to 'contrib/subtac')
| -rw-r--r-- | contrib/subtac/eterm.ml | 2 | ||||
| -rw-r--r-- | contrib/subtac/infer.ml | 4 | ||||
| -rw-r--r-- | contrib/subtac/rewrite.ml | 11 |
3 files changed, 10 insertions, 7 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 4f86af1e8..7b07abbc8 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -61,7 +61,7 @@ let etype_of_evar evs ev = | [] -> let t' = subst_evars evs n ev.evar_concl in subst_vars acc 0 t' - in aux [] 0 (rev ev.evar_hyps) + in aux [] 0 (rev (Environ.named_context_of_val ev.evar_hyps)) open Tacticals diff --git a/contrib/subtac/infer.ml b/contrib/subtac/infer.ml index dcca9361a..876dc68bb 100644 --- a/contrib/subtac/infer.ml +++ b/contrib/subtac/infer.ml @@ -552,7 +552,7 @@ let rec dtype_of_types ctx c = | Meta mv -> notimpl "Meta" | Evar pex -> notimpl "Evar" | Sort s -> DTSort (dummy_loc, s) - | Cast (c, t) -> snd (dtype_of_types ctx t) + | Cast (c, _, t) -> snd (dtype_of_types ctx t) | Prod (n, t, t') -> let dt = dtype_of_types ctx t in let ctx' = (n, dt) :: ctx in @@ -600,7 +600,7 @@ let rec dtype_of_constr ctx c = | Meta mv -> notimpl "Meta" | Evar pex -> notimpl "Evar" | Sort s -> DTSort (dummy_loc, s) - | Cast (c, t) -> snd (dtype_of_constr ctx t) + | Cast (_,_,t) -> snd (dtype_of_constr ctx t) | Prod (n, t, t') -> let dt = dtype_of_constr ctx t in let ctx' = (n, dt) :: ctx in diff --git a/contrib/subtac/rewrite.ml b/contrib/subtac/rewrite.ml index c9a0a78c7..ce0f15ec2 100644 --- a/contrib/subtac/rewrite.ml +++ b/contrib/subtac/rewrite.ml @@ -349,7 +349,8 @@ and subset_coerce prog_info ctx x y = let ctx', pcx' = subst_ctx ctx pcx in cx, { Evd.evar_concl = pcx'; - Evd.evar_hyps = evar_ctx prog_info ctx'; + Evd.evar_hyps = + Environ.val_of_named_context (evar_ctx prog_info ctx'); Evd.evar_body = Evd.Evar_empty; } in @@ -368,7 +369,7 @@ and subset_coerce prog_info ctx x y = in ignore(Univ.merge_constraints cstrs (Global.universes ())); Some (fun x -> - mkCast (x, y)) + mkCast (x, DEFAULTcast, y)) with Reduction.NotConvertible -> subtyping_error @@ -420,7 +421,9 @@ and rewrite_term prog_info ctx (t : dterm_loc) : Term.constr * Term.types = let evarinfo = { Evd.evar_concl = proof; - Evd.evar_hyps = evar_ctx prog_info ctx'; + Evd.evar_hyps = + Environ.val_of_named_context + (evar_ctx prog_info ctx'); Evd.evar_body = Evd.Evar_empty; } in @@ -581,7 +584,7 @@ let subtac recursive id (s, t) = let key = mknewexist () in prog_info.evm <- Evd.add prog_info.evm key { Evd.evar_concl = wf_rel; - Evd.evar_hyps = []; + Evd.evar_hyps = Environ.empty_named_context_val; Evd.evar_body = Evd.Evar_empty }; mkEvar (key, [| |]) in |