From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 9 Jun 2005 11:45:45 +0000 (+0000)
Subject: added whd before uri_of_term
X-Git-Tag: PRE_INDEX_1~16
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a092d97f720a9241d77d987a72cdb810c1d88212;p=helm.git

added whd before uri_of_term
---

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 3c141126d..eb3193264 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -226,8 +226,15 @@ let eval_coercion status coercion =
     aux ty
   in
   let ty_src,ty_tgt = extract_last_two_p coer_ty in
-  let src_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_src) in
-  let tgt_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) in
+  let context = [] in 
+  let src_uri = 
+    let ty_src = CicReduction.whd context ty_src in
+    UriManager.uri_of_string (CicUtil.uri_of_term ty_src) 
+  in
+  let tgt_uri = 
+    let ty_tgt = CicReduction.whd context ty_tgt in
+    UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) 
+  in
   let new_coercions =
     (* also adds them to the Db *)
     CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri