diff options
| author | barras | 2001-10-09 16:40:03 +0000 |
|---|---|---|
| committer | barras | 2001-10-09 16:40:03 +0000 |
| commit | f1778f0e830c50aaec250916f14e202d95960414 (patch) | |
| tree | ae220556180dfa55d6b638467deb7edf58d4c17b /kernel/names.ml | |
| parent | 8dbab7f463cabfc2913ab8615973c96ac98bf371 (diff) | |
Suppression des arguments sur les constantes, inductifs et constructeurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 3d72326edb..811672ba3d 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -316,11 +316,11 @@ module Spmap = Map.Make(SpOrdered) (* Special references for inductive objects *) -type variable_path = section_path -type constant_path = section_path -type inductive_path = section_path * int -type constructor_path = inductive_path * int -type mutual_inductive_path = section_path +type variable = section_path +type constant = section_path +type inductive = section_path * int +type constructor = inductive * int +type mutual_inductive = section_path (* Hash-consing of name objects *) module Hname = Hashcons.Make( |