From a092d97f720a9241d77d987a72cdb810c1d88212 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 9 Jun 2005 11:45:45 +0000 Subject: [PATCH] added whd before uri_of_term --- helm/matita/matitaEngine.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) 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 -- 2.39.2