From edfda2501f08f18e24bd2e3eca763eb1c2dec0ea Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 18 Oct 2000 17:51:58 +0000
Subject: Simplifications autour de typed_type (renommé types par analogie avec
 sorts); documentation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/class.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'pretyping/class.ml')

diff --git a/pretyping/class.ml b/pretyping/class.ml
index b83eb3608f..0f201d004f 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -285,14 +285,12 @@ lorque source est None alors target est None aussi.
 let try_add_new_coercion_core idf stre source target isid =
   let env = Global.env () in
   let v = construct_reference env CCI idf in
-  let t = Retyping.get_type_of env Evd.empty v in
-  let k = Retyping.get_sort_of env Evd.empty t in
-  let vj = {uj_val=v; uj_type= make_typed t k} in
+  let vj = Retyping.get_judgment_of env Evd.empty v in
   let f_vardep,coef = coe_of_reference v in
   if coercion_exists coef then
     errorlabstrm "try_add_coercion" 
       [< 'sTR(string_of_id idf) ; 'sTR" is already a coercion" >];
-  let lp = prods_of t in
+  let lp = prods_of (vj.uj_type) in
   let llp = List.length lp in
   if llp <= 1 then
     errorlabstrm "try_add_coercion"         
-- 
cgit v1.2.3