diff options
| author | gregoire | 2005-12-02 10:01:15 +0000 |
|---|---|---|
| committer | gregoire | 2005-12-02 10:01:15 +0000 |
| commit | bf578ad5e2f63b7a36aeaef5e0597101db1bd24a (patch) | |
| tree | c0bc4e5f9ae67b8a03b28134dab3dcfe31d184dd /contrib/subtac | |
| parent | 825a338a1ddf1685d55bb5193aa5da078a534e1c (diff) | |
Changement des named_context
Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
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 4f86af1e81..7b07abbc8e 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 dcca9361ae..876dc68bba 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 c9a0a78c75..ce0f15ec28 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 |