diff options
| author | barras | 2001-05-03 09:54:17 +0000 |
|---|---|---|
| committer | barras | 2001-05-03 09:54:17 +0000 |
| commit | bf352b0b29a8e3d55eaa986c4f493af48f8ddf52 (patch) | |
| tree | b0633f3a1ee73bd685327c2c988426d65de7a58a /kernel/term.mli | |
| parent | c4a517927f148e0162d22cb7077fa0676d799926 (diff) | |
Changement de la structure des points fixes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index c8f6ea4a14..e873525cee 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -48,7 +48,7 @@ type 'constr constant = constant_path * 'constr array type 'constr constructor = constructor_path * 'constr array type 'constr inductive = inductive_path * 'constr array type ('constr, 'types) rec_declaration = - 'types array * name list * 'constr array + name array * 'types array * 'constr array type ('constr, 'types) fixpoint = (int array * int) * ('constr, 'types) rec_declaration type ('constr, 'types) cofixpoint = @@ -124,7 +124,7 @@ type existential = existential_key * constr array type constant = constant_path * constr array type constructor = constructor_path * constr array type inductive = inductive_path * constr array -type rec_declaration = types array * name list * constr array +type rec_declaration = name array * types array * constr array type fixpoint = (int array * int) * rec_declaration type cofixpoint = int * rec_declaration @@ -561,7 +561,7 @@ type constr_operator = | OpMutInd of inductive_path | OpMutConstruct of constructor_path | OpMutCase of case_info - | OpRec of fix_kind * Names.name list + | OpRec of fix_kind * name array val splay_constr : constr -> constr_operator * constr array |