From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 24 Jul 2009 22:05:07 +0000 (+0000)
Subject: Record fields declared as coercions as now really declared as coercions.
X-Git-Tag: make_still_working~3621
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1836052e4215c79479f616de6c71cf36f01c8216;p=helm.git

Record fields declared as coercions as now really declared as coercions.
---

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 5d1b81d74..be069fce1 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -702,6 +702,12 @@ let src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt =
   status, src, tgt, cpos, arity
 ;;
 
+let basic_eval_and_inject_ncoercion infos status =
+ let status = basic_eval_ncoercion infos status in
+ let dump = inject_ncoercion infos::status#dump in
+  status#set_dump dump
+;;
+
 let eval_ncoercion status name t ty (id,src) tgt = 
 
  let metasenv,subst,status,ty =
@@ -714,12 +720,10 @@ let eval_ncoercion status name t ty (id,src) tgt =
  let t = NCicUntrusted.apply_subst subst [] t in
 
  let status, src, tgt, cpos, arity = 
-   src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt
+   src_tgt_cpos_arity_of_ty_id_src_tgt status ty id src tgt in
+ let status =
+  basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity) status
  in
-
- let status = basic_eval_ncoercion (name,t,src,tgt,cpos,arity) status in
- let dump = inject_ncoercion (name,t,src,tgt,cpos,arity)::status#dump in
- let status = status#set_dump dump in
   status,`New []
 ;;
 
@@ -1010,8 +1014,15 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
            let status =
             List.fold_left
              (fun status (name,cpos,arity) ->
-                (*CSC: COME DICHIARO LA COERCION??? *)
-                status
+               let metasenv,subst,status,t =
+                GrafiteDisambiguate.disambiguate_nterm None status [] [] []
+                 ("",0,CicNotationPt.Ident (name,None)) in
+               assert (metasenv = [] && subst = []);
+               let ty = NCicTypeChecker.typeof ~subst ~metasenv [] t in
+               let src,tgt = src_tgt_of_ty_cpos_arity ty cpos arity in
+prerr_endline ("COERCION " ^ name ^ " cpos = " ^ string_of_int cpos ^ " arity = " ^ string_of_int arity);
+                basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity)
+                 status
              ) status coercions
            in
             status,uris