X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTacStatus.ml;h=31260d5ed837ea595caa9bf49944b60567edbb0a;hb=bbf85ddcdfe0809fee0c6ca9812ce0da30c238af;hp=1001d980854605340166d0e8cb7055d5d876665e;hpb=90e823f96159811d88b275df9c3ec9a4c40ff816;p=helm.git diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml index 1001d9808..31260d5ed 100644 --- a/matita/components/ng_tactics/nTacStatus.ml +++ b/matita/components/ng_tactics/nTacStatus.ml @@ -48,7 +48,7 @@ class eq_status = method eq_cache = eq_cache method set_eq_cache v = {< eq_cache = v >} method set_eq_status - : 'status. #g_eq_status as 'status -> 'self + : 'status. (#g_eq_status as 'status) -> 'self = fun o -> self#set_eq_cache o#eq_cache end @@ -63,7 +63,7 @@ class auto_status = method auto_cache = auto_cache method set_auto_cache v = {< auto_cache = v >} method set_auto_status - : 'status. #g_auto_status as 'status -> 'self + : 'status. (#g_auto_status as 'status) -> 'self = fun o -> self#set_auto_cache o#auto_cache end @@ -84,7 +84,7 @@ class virtual pstatus = val obj = o method obj = obj method set_obj o = {< obj = o >} - method set_pstatus : 'status. #g_pstatus as 'status -> 'self + method set_pstatus : 'status. (#g_pstatus as 'status) -> 'self = fun o -> (((self#set_disambiguate_status o)#set_obj o#obj)#set_auto_status o)#set_eq_status o end @@ -97,24 +97,24 @@ let ctx_of (c,_) = c ;; let mk_cic_term c t = c,t ;; let ppterm (status:#pstatus) t = - let uri,height,metasenv,subst,obj = status#obj in + let _uri,_height,metasenv,subst,_obj = status#obj in let context,t = t in status#ppterm ~metasenv ~subst ~context t ;; let ppcontext (status: #pstatus) c = - let uri,height,metasenv,subst,obj = status#obj in + let _uri,_height,metasenv,subst,_obj = status#obj in status#ppcontext ~metasenv ~subst c ;; let ppterm_and_context (status: #pstatus) t = - let uri,height,metasenv,subst,obj = status#obj in + let _uri,_height,metasenv,subst,_obj = status#obj in let context,t = t in status#ppcontext ~metasenv ~subst context ^ "\n ⊢ "^ status#ppterm ~metasenv ~subst ~context t ;; -let relocate status destination (source,t as orig) = +let relocate status destination (source,_t as orig) = pp(lazy("relocate:\n" ^ ppterm_and_context status orig)); pp(lazy("relocate in:\n" ^ ppcontext status destination)); let rc = @@ -134,13 +134,13 @@ let relocate status destination (source,t as orig) = compute_ops (e::ctx) (cl1,cl2) else [ `Delift ctx; `Lift (List.rev ex) ] - | (n1, NCic.Def (b1,t1) as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 -> + | (n1, NCic.Def (_b1,t1) as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 -> if n1 = n2 && NCicReduction.are_convertible status ctx ~subst ~metasenv t1 t2 then compute_ops (e::ctx) (cl1,cl2) else [ `Delift ctx; `Lift (List.rev ex) ] - | (n1, NCic.Decl _)::cl1 as ex, (n2, NCic.Def _)::cl2 -> + | (_n1, NCic.Decl _)::_cl1 as ex, (_n2, NCic.Def _)::_cl2 -> [ `Delift ctx; `Lift (List.rev ex) ] | _::_ as ex, [] -> [ `Lift (List.rev ex) ] | [], _::_ -> [ `Delift ctx ] @@ -235,7 +235,7 @@ let normalize status ?delta ctx t = let are_convertible status ctx a b = let status, (_,a) = relocate status ctx a in let status, (_,b) = relocate status ctx b in - let n,h,metasenv,subst,o = status#obj in + let _n,_h,metasenv,subst,_o = status#obj in let res = NCicReduction.are_convertible status metasenv subst ctx a b in status, res ;; @@ -293,7 +293,7 @@ let get_subst status = let to_subst status i entry = let name,height,metasenv,subst,obj = status#obj in - let metasenv = List.filter (fun j,_ -> j <> i) metasenv in + let metasenv = List.filter (fun (j,_) -> j <> i) metasenv in let subst = (i, entry) :: subst in status#set_obj (name,height,metasenv,subst,obj) ;; @@ -334,7 +334,7 @@ let mk_meta status ?(attrs=[]) ctx bo_or_ty kind = let metasenv, metano, instance, _ = NCicMetaSubst.mk_meta ~attrs metasenv ctx ~with_type:ty kind in let attrs,_,_ = NCicUtils.lookup_meta metano metasenv in - let metasenv = List.filter (fun j,_ -> j <> metano) metasenv in + let metasenv = List.filter (fun (j,_) -> j <> metano) metasenv in let subst = (metano, (attrs, ctx, bo_, ty)) :: subst in let status = status#set_obj (n,h,metasenv,subst,o) in status, (ctx,instance) @@ -378,7 +378,7 @@ let select_term else let _,_,_,subst,_ = status#obj in match t with - | NCic.Meta (i,lc) when List.mem_assoc i subst -> + | NCic.Meta (i,_lc) when List.mem_assoc i subst -> let _,_,t,_ = NCicUtils.lookup_subst i subst in aux ctx (status,already_found) t | NCic.Meta _ -> (status,already_found),t @@ -503,17 +503,17 @@ class virtual ['stack] status = val stack = s method stack = stack method set_stack s = {< stack = s >} - method set_status : 'status. 'stack #g_status as 'status -> 'self + method set_status : 'status. ('stack #g_status as 'status) -> 'self = fun o -> (self#set_pstatus o)#set_stack o#stack end class type virtual lowtac_status = [unit] status -type 'status lowtactic = #lowtac_status as 'status -> int -> 'status +type 'status lowtactic = (#lowtac_status as 'status) -> int -> 'status class type virtual tac_status = [Continuationals.Stack.t] status -type 'status tactic = #tac_status as 'status -> 'status +type 'status tactic = (#tac_status as 'status) -> 'status let pp_tac_status (status: #tac_status) = prerr_endline (status#ppobj status#obj); @@ -568,8 +568,8 @@ let compare e1 e2 = match e1,e2 with | Constant (u1,a1),Constant (u2,a2) -> let x = NUri.compare u1 u2 in - if x = 0 then Pervasives.compare a1 a2 else x - | e1,e2 -> Pervasives.compare e1 e2 + if x = 0 then Stdlib.compare a1 a2 else x + | e1,e2 -> Stdlib.compare e1 e2 ;; @@ -578,7 +578,7 @@ end module Ncic_termOT : Set.OrderedType with type t = cic_term = struct type t = cic_term - let compare = Pervasives.compare + let compare = Stdlib.compare end module Ncic_termSet : Set.S with type elt = cic_term = Set.Make(Ncic_termOT)