diff options
| author |  gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-05 10:16:24 +0000 |
|---|---|---|
| committer | gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-05 10:16:24 +0000 |
| commit | a3508843fa932cbc9a3c0b0d3dc5004752d2a8e4 (patch) | |
| tree | 65d41498a65f229c9c77ad1a9b48a4059422b8cd /kernel/vm.ml | |
| 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/vm.ml')
| -rw-r--r-- | kernel/vm.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/vm.ml b/kernel/vm.ml index 8f0d2ebdd..c8be979e0 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 |