Datatypes.length and app defined back via fun+fix instead of Fixpoint

  Since length and app were defined inside a Section in List.v,
  their type argument A wasn't inside the fixpoint. Restoring
  the initial definition repairs (at least) Cachan/IntMap.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12477 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 2 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 78d0110ae..fc64f081b 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -250,7 +250,8 @@ Bind Scope list_scope with list.
 
 Local Open Scope list_scope.
 
-Fixpoint length (A : Type) (l:list A) : nat :=
+Definition length (A : Type) : list A -> nat :=
+  fix length l :=
   match l with
    | nil => O
    | _ :: l' => S (length l')
@@ -258,7 +259,8 @@ Fixpoint length (A : Type) (l:list A) : nat :=
 
 (** Concatenation of two lists *)
 
-Fixpoint app (A : Type) (l m:list A) : list A :=
+Definition app (A : Type) : list A -> list A -> list A :=
+  fix app l m :=
   match l with
    | nil => m
    | a :: l1 => a :: app l1 m