From c1db8eb695a04d172130959ff38eef61d3ca9653 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 31 Jan 2001 11:29:28 +0000
Subject: Bug lié au discharge

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1300 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/class.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 587caae76e..40ecc11c38 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -459,6 +459,7 @@ let process_cl sec_sp cl =
 
 (* Pour le discharge *)
 let process_coercion sec_sp (((coe,coeinfo),s,t) as x) =
+  (* Buggé: faut mettre à jour le nombre de paramètres dans coeinfo *)
   let s1= process_cl sec_sp s in
   let t1 = process_cl sec_sp t in
   match coe with 
-- 
cgit v1.2.3