diff options
| author | gregoire | 2005-12-05 10:16:24 +0000 |
|---|---|---|
| committer | gregoire | 2005-12-05 10:16:24 +0000 |
| commit | a3508843fa932cbc9a3c0b0d3dc5004752d2a8e4 (patch) | |
| tree | 65d41498a65f229c9c77ad1a9b48a4059422b8cd /kernel | |
| parent | bf578ad5e2f63b7a36aeaef5e0597101db1bd24a (diff) | |
changement d'egalite pour le named_context_val
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7640 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 3 | ||||
| -rw-r--r-- | kernel/environ.mli | 2 | ||||
| -rw-r--r-- | kernel/vm.ml | 5 |
3 files changed, 8 insertions, 2 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 45ae911a25..0555096e24 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -106,6 +106,9 @@ let val_of_named_context ctxt = let lookup_named id env = Sign.lookup_named id env.env_named_context let lookup_named_val id (ctxt,_) = Sign.lookup_named id ctxt +let eq_named_context_val c1 c2 = + c1 == c2 || named_context_of_val c1 = named_context_of_val c2 + (* A local const is evaluable if it is defined *) let named_type id env = diff --git a/kernel/environ.mli b/kernel/environ.mli index b8f565e45c..1b1e227bb2 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -37,6 +37,7 @@ type env val pre_env : env -> Pre_env.env type named_context_val +val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env @@ -45,6 +46,7 @@ val rel_context : env -> rel_context val named_context : env -> named_context val named_context_val : env -> named_context_val + val engagement : env -> engagement option (* is the local context empty *) diff --git a/kernel/vm.ml b/kernel/vm.ml index 8f0d2ebddd..c8be979e0d 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -76,9 +76,9 @@ let crasy_val = (val_of_obj (repr 0)) (* Functions *) type vfun (* v = [Tc | c | fv1 | ... | fvn ] *) -(* ^ *) +(* ^ *) (* [Tc | (Restart : c) | v | a1 | ... an] *) -(* ^ *) +(* ^ *) (* Products *) type vprod @@ -220,6 +220,7 @@ type vswitch = { sw_env : vm_env } +(* Ne pas changer ce type sans modifier le code C *) type atom = | Aid of id_key | Aiddef of id_key * values |