From ee49451b4b4f507835752d38f89cb67abd4e2361 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 5 Feb 2001 23:28:09 +0000
Subject: Restructuration de classops; évolution en une version mieux intégrée
 au reste du système; conséquences collatérales

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1329 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/coercion.ml | 2 +-
 toplevel/recordobj.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 428af0a4a8..bd25f93518 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -49,7 +49,7 @@ let apply_coercion env p hj typ_cl =
   try 
     fst (List.fold_left
            (fun (ja,typ_cl) i -> 
-              let fv,b = coe_value i in
+              let fv,b = coercion_value i in
               let argl = (class_args_of typ_cl)@[ja.uj_val] in
               let jres = apply_coercion_args env argl fv in
               (if b then 
diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml
index 5e54d1ffa1..a5556e6e61 100755
--- a/toplevel/recordobj.ml
+++ b/toplevel/recordobj.ml
@@ -75,6 +75,6 @@ let objdef_declare ref =
         List.iter 
 	  (fun (spi,(ci,l_ui)) -> 
 	     add_new_objdef 
-	       ((NAM_Constant spi,cte_of_constr ci),v,lt,params,l_ui)) comp
+	       ((ConstRef spi,cte_of_constr ci),v,lt,params,l_ui)) comp
     | _ -> objdef_err ref
                  
-- 
cgit v1.2.3