X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=0523ef8b202fae7e1c406b8758e5b8be78651581;hb=0af3592e3a85a4bb82c5c6df259cf9ab117ba0b1;hp=af8e1d87a1f31c62dded9015374d1786258bd117;hpb=f7da48c844105a52a705872dfa0d4104de010c82;p=helm.git

diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml
index af8e1d87a..0523ef8b2 100644
--- a/matita/components/ng_refiner/nCicRefiner.ml
+++ b/matita/components/ng_refiner/nCicRefiner.ml
@@ -178,6 +178,16 @@ in
   name' ^ (if last = -1 then "" else string_of_int (last + 1))
 with exn -> prerr_endline ("XXX" ^ Printexc.to_string exn); assert false
 
+(* let eq, eq_refl =
+    let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
+    C.Const (Ref.reference_of_spec uri (Ref.Ind (true,0,2))),
+    C.Const (Ref.reference_of_spec uri Ref.Con (0,1,2))
+*)
+let eq, eq_refl = 
+ let uri = NUri.uri_of_string "cic:/matita/basics/jmeq/jmeq.ind" in
+ C.Const (Ref.reference_of_spec uri (Ref.Ind(true,0,2))),
+ C.Const (Ref.reference_of_spec uri (Ref.Con(0,1,2)))
+
 let rec typeof (status:#NCicCoercion.status)
   ?(localise=fun _ -> Stdpp.dummy_loc) 
   metasenv subst context term expty 
@@ -598,15 +608,15 @@ and try_coercions status
     pp (lazy "WWW: trying coercions -- inner check");
     match infty, expty, t with
     (* `XTSort|`XTProd|`XTInd + Match not implemented *) 
-    | _,`XTSome expty, C.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) ->
+    | _,`XTSome expty, C.Match (Ref.Ref (_,Ref.Ind (_,_tyno,_leftno)) as r,outty,m,pl) ->
         (*{{{*) pp (lazy "CASE");
         (* {{{ helper functions *)
         let get_cl_and_left_p refit outty =
           match refit with
-          | NReference.Ref (uri, NReference.Ind (_,tyno,leftno)) ->
+          | Ref.Ref (_uri, Ref.Ind (_,tyno,_leftno)) ->
              let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys status r in
              let _, _, ty, cl = List.nth itl tyno in
-             let constructorsno = List.length cl in
+             (*let constructorsno = List.length cl in*)
               let count_pis t =
                 let rec aux ctx t = 
                   match NCicReduction.whd status ~subst ~delta:max_int ctx t with
@@ -678,10 +688,6 @@ and try_coercions status
                 (List.map (NCicSubstitution.lift status 1) right_p) (NCicSubstitution.lift status 1 matched) (n-1))
           | _ -> assert false
         in
-        (*let eq = C.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in
-        let eq_refl = C.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*)
-        let eq = C.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.ind(1,0,2)")) in
-        let eq_refl = C.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.con(0,1,2)")) in
         let add_params 
           metasenv subst context cty outty mty m i 
         =
@@ -694,7 +700,7 @@ and try_coercions status
                     (NCicSubstitution.lift status 1 mty) (NCicSubstitution.lift status 1 m) tgt
                 in
                 C.Prod (name, src, t), k
-            | C.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r) ->
+            | C.Const (Ref.Ref (_,Ref.Ind (_,_,_leftno)) as r) ->
                 let k = 
                   let k = C.Const(Ref.mk_constructor i r) in
                   NCicUntrusted.mk_appl k par
@@ -710,8 +716,8 @@ and try_coercions status
                   (NCicReduction.head_beta_reduce status ~delta:max_int 
                    (NCicUntrusted.mk_appl outty [k])))),[mty,m,mty,k]
             | C.Appl (C.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r)::pl) ->
-                let left_p,right_p = HExtlib.split_nth leftno pl in
-                let has_rights = right_p <> [] in
+                let left_p,_right_p = HExtlib.split_nth leftno pl in
+                (*let has_rights = right_p <> [] in*)
                 let k = 
                   let k = C.Const(Ref.mk_constructor i r) in
                   NCicUntrusted.mk_appl k (left_p@par)
@@ -813,7 +819,7 @@ and try_coercions status
         in (* }}} end helper functions *)
         (* constructors types with left params already instantiated *)
         let outty = NCicUntrusted.apply_subst status subst context outty in
-        let cl, left_p, leftno,rno = 
+        let cl, _left_p, leftno,rno = 
           get_cl_and_left_p r outty
         in
         let right_p, mty = 
@@ -924,7 +930,7 @@ and try_coercions status
         pp (lazy ("LAM: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced));
         metasenv, subst, coerced, expty (*}}}*)
     | _ -> raise exc
-  with exc2 ->    
+  with _ ->    
   let expty =
    match expty with
       `XTSome expty -> expty
@@ -934,6 +940,7 @@ and try_coercions status
            | x::_ -> x 
            | _ -> assert false))
     | `XTProd -> C.Prod ("_",C.Implicit `Type,C.Implicit `Type)
+    | `XTInd -> assert false(*CSC: was not handled, OCaml 4.0 complains. ??? *)
   in
   pp(lazy("try_coercion " ^ 
     status#ppterm ~metasenv ~subst ~context infty ^ " |---> " ^
@@ -1013,8 +1020,8 @@ and sort_of_prod status localise metasenv subst context orig_s orig_t (name,s)
 and guess_name status subst ctx ty = 
   let aux initial = "#" ^ String.make 1 initial in
   match ty with
-  | C.Const (NReference.Ref (u,_))
-  | C.Appl (C.Const (NReference.Ref (u,_)) :: _) ->
+  | C.Const (Ref.Ref (u,_))
+  | C.Appl (C.Const (Ref.Ref (u,_)) :: _) ->
       aux (String.sub (NUri.name_of_uri u) 0 1).[0] 
   | C.Prod _ -> aux 'f' 
   | C.Meta (n,lc) -> 
@@ -1105,7 +1112,7 @@ and eat_prods status ~localise force_ty metasenv subst context expty orig_t orig
           aux metasenv subst (arg :: args_so_far) he meta tl
       | C.Match (_,_,C.Meta _,_) 
       | C.Match (_,_,C.Appl (C.Meta _ :: _),_) 
-      | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) ->
+      | C.Appl (C.Const (Ref.Ref (_, Ref.Fix _)) :: _) ->
           raise (Uncertain (lazy (localise orig_he, Printf.sprintf
             ("The term %s is here applied to %d arguments but expects " ^^
             "only %d arguments") (status#ppterm ~metasenv ~subst ~context he)
@@ -1170,8 +1177,8 @@ let undebruijnate status inductive ref t rev_fl =
       (fun (_,_,rno,_,_,_) i -> 
          let i = len - i - 1 in
          C.Const 
-           (if inductive then NReference.mk_fix i rno ref
-            else NReference.mk_cofix i ref))
+           (if inductive then Ref.mk_fix i rno ref
+            else Ref.mk_cofix i ref))
       rev_fl)
     t
 ;; 
@@ -1223,9 +1230,9 @@ let typeof_obj
           (fun (relevance,name,k,ty,dbo) ->
             let bo = 
               undebruijnate status inductive 
-               (NReference.reference_of_spec uri 
-                 (if inductive then NReference.Fix (0,k,0) 
-                  else NReference.CoFix 0)) dbo rev_fl
+               (Ref.reference_of_spec uri 
+                 (if inductive then Ref.Fix (0,k,0) 
+                  else Ref.CoFix 0)) dbo rev_fl
             in
               relevance,name,k,ty,bo)
           fl
@@ -1305,7 +1312,7 @@ let typeof_obj
                 let rec aux context (metasenv,subst) = function
                   | C.Meta _ -> metasenv, subst
                   | C.Implicit _ -> metasenv, subst
-                  | C.Appl (C.Rel i :: args) as t
+                  | C.Appl (C.Rel i :: args)
                       when i > List.length context - len ->
                       let lefts, _ = HExtlib.split_nth leftno args in
                       let ctxlen = List.length context in
@@ -1364,8 +1371,8 @@ let typeof_obj
                     if i <= leftno  then
                      C.Rel i
                     else
-                     C.Const (NReference.reference_of_spec uri
-                      (NReference.Ind (ind,relsno - i,leftno))))
+                     C.Const (Ref.reference_of_spec uri
+                      (Ref.Ind (ind,relsno - i,leftno))))
                   (HExtlib.list_seq 1 (relsno+1))
                    te in
                let te =