diff options
author | 2001-05-03 09:54:17 +0000 | |
---|---|---|
committer | 2001-05-03 09:54:17 +0000 | |
commit | bf352b0b29a8e3d55eaa986c4f493af48f8ddf52 (patch) | |
tree | b0633f3a1ee73bd685327c2c988426d65de7a58a /kernel/closure.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/closure.mli')
-rw-r--r-- | kernel/closure.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli index 45088b3ac..3d8fb71f3 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -145,9 +145,9 @@ type fterm = | FInd of inductive_path * fconstr array | FConstruct of constructor_path * fconstr array | FApp of fconstr * fconstr array - | FFix of (int array * int) * (fconstr array * name list * fconstr array) + | FFix of (int array * int) * (name array * fconstr array * fconstr array) * constr array * fconstr subs - | FCoFix of int * (fconstr array * name list * fconstr array) + | FCoFix of int * (name array * fconstr array * fconstr array) * constr array * fconstr subs | FCases of case_info * fconstr * fconstr * fconstr array | FLambda of name * fconstr * fconstr * constr * fconstr subs |