From c83721701dbbd44d3d547fdec6c4a5658322f424 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 13 Jul 2009 03:27:46 +0000 Subject: [PATCH] Coercion hiding implemented. Notes: 1) hiding of coercions whose return type is a product is not done correctly, since the "sats" information seem to have changed semantics. Enrico, is it a bug or just a new semantics? 2) coercion matching has been implemented trivially (O(n)) in NCicCoercion. Here I need a special version of a discrimination tree. Enrico, do we have one already or is there a way to simulate it? --- .../METAS/meta.helm-ng_cic_content.src | 2 +- helm/software/components/Makefile | 2 +- .../acic_content/termAcicContent.ml | 4 +- .../components/binaries/transcript/.depend | 5 ++ .../components/extlib/discrimination_tree.ml | 3 ++ .../components/extlib/discrimination_tree.mli | 1 + helm/software/components/extlib/hExtlib.mli | 6 +-- .../ng_cic_content/nTermCicContent.ml | 50 +++++++++++++------ .../ng_cic_content/nTermCicContent.mli | 9 ++-- .../components/ng_refiner/nCicCoercion.ml | 28 +++++++++++ .../components/ng_refiner/nCicCoercion.mli | 5 ++ helm/software/matita/applyTransformation.ml | 8 +-- helm/software/matita/applyTransformation.mli | 3 +- helm/software/matita/matita.ml | 6 +-- helm/software/matita/matitaGuiTypes.mli | 11 ++-- helm/software/matita/matitaMathView.ml | 47 ++++++++++------- .../matita/nlibrary/algebra/magmas.ma | 2 +- 17 files changed, 137 insertions(+), 55 deletions(-) diff --git a/helm/software/components/METAS/meta.helm-ng_cic_content.src b/helm/software/components/METAS/meta.helm-ng_cic_content.src index fb48b84b3..4823c8bc6 100644 --- a/helm/software/components/METAS/meta.helm-ng_cic_content.src +++ b/helm/software/components/METAS/meta.helm-ng_cic_content.src @@ -1,4 +1,4 @@ -requires="helm-library helm-acic_content helm-ng_kernel" +requires="helm-library helm-acic_content helm-ng_refiner" version="0.0.1" archive(byte)="ng_cic_content.cma" archive(native)="ng_cic_content.cmxa" diff --git a/helm/software/components/Makefile b/helm/software/components/Makefile index 51b2f4bbf..b7c105fc0 100644 --- a/helm/software/components/Makefile +++ b/helm/software/components/Makefile @@ -26,6 +26,7 @@ MODULES = \ ng_kernel \ acic_content \ grafite \ + ng_refiner \ ng_cic_content \ content_pres \ cic_unification \ @@ -35,7 +36,6 @@ MODULES = \ disambiguation \ cic_disambiguation \ lexicon \ - ng_refiner \ ng_disambiguation \ grafite_parser \ ng_paramodulation \ diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index 0af74d261..81d0ef0a7 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -154,11 +154,11 @@ let ast_of_acic0 ~output_type term_info acic k = try HExtlib.split_nth (cpos+sats+1) tl with Failure _ -> [],[] in if rest = [] then - idref aid (List.nth (List.map k tl) cpos) + idref aid (k (List.nth tl cpos)) else idref aid (Ast.Appl (List.map k (List.nth tl cpos::rest))) else - idref aid (Ast.Appl (List.map k tl)) + idref aid (Ast.Appl (List.map k args)) else idref aid (Ast.Appl (List.map k args))) | Cic.AAppl (aid,args) -> diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index bb6f22a64..87d1ed25c 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,6 +1,11 @@ gallina8Parser.cmi: types.cmo grafiteParser.cmi: types.cmo grafite.cmi: types.cmo +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmo gallina8Parser.cmi diff --git a/helm/software/components/extlib/discrimination_tree.ml b/helm/software/components/extlib/discrimination_tree.ml index e0803c350..f96a0de56 100644 --- a/helm/software/components/extlib/discrimination_tree.ml +++ b/helm/software/components/extlib/discrimination_tree.ml @@ -62,6 +62,7 @@ module type DiscriminationTree = type t val iter : t -> (constant_name path -> dataset -> unit) -> unit + val fold : t -> (constant_name path -> dataset -> 'b -> 'b) -> 'b -> 'b val empty : t val index : t -> input -> data -> t @@ -99,6 +100,8 @@ and type data = A.elt and type dataset = A.t = let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;; + let fold dt f = DiscriminationTree.fold (fun p x -> f p x) dt;; + let index tree term info = let ps = I.path_string_of term in let ps_set = diff --git a/helm/software/components/extlib/discrimination_tree.mli b/helm/software/components/extlib/discrimination_tree.mli index e979b8e69..4c8339e5e 100644 --- a/helm/software/components/extlib/discrimination_tree.mli +++ b/helm/software/components/extlib/discrimination_tree.mli @@ -55,6 +55,7 @@ module type DiscriminationTree = type t val iter : t -> (constant_name path -> dataset -> unit) -> unit + val fold : t -> (constant_name path -> dataset -> 'b -> 'b) -> 'b -> 'b val empty : t val index : t -> input -> data -> t diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli index 9c0980f76..f5e3741d4 100644 --- a/helm/software/components/extlib/hExtlib.mli +++ b/helm/software/components/extlib/hExtlib.mli @@ -106,14 +106,14 @@ val sharing_map: ('a -> 'a) -> 'a list -> 'a list The second one can be shorter and is padded with a default value. This function cannot fail. *) val list_iter_default2: ('a -> 'b -> unit) -> 'a list -> 'b -> 'b list -> unit +exception FailureAt of int (* Checks a predicate in parallel on three lists, the first two having the same length (otherwise it raises Invalid_argument). It stops when the first two - lists are empty. The third one can be shorter and is padded with a default value. *) + lists are empty. The third one can be shorter and is padded with a default + value. It can also raise FailureAt when ??? *) val list_forall_default3: ('a -> 'b -> 'c -> bool) -> 'a list -> 'b list -> 'c -> 'c list -> bool val list_forall_default3_var: ('a -> 'b -> 'c -> bool) -> 'a list -> 'b list -> 'c -> 'c list -> bool -exception FailureAt of int - (** split_nth n l * @returns two list, the first contains at least n elements, the second the * remaining ones diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml index 01e6fd482..8984a4829 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.ml +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -59,10 +59,10 @@ let idref register_ref = ;; (* CODICE c&p da NCicPp *) -let nast_of_cic0 +let nast_of_cic0 status ~(idref: ?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term) - ~output_type ~subst k ~context = + ~output_type ~metasenv ~subst k ~context = function | NCic.Rel n -> (try @@ -113,7 +113,26 @@ let nast_of_cic0 (match hd with | NCic.Appl l -> NCic.Appl (l@args) | _ -> NCic.Appl (hd :: args))) - | NCic.Appl args -> idref (Ast.Appl (List.map (k ~context) args)) + | NCic.Appl args as t -> + let args = + if not !Acic2content.hide_coercions then args + else + match + NCicCoercion.match_coercion status ~metasenv ~context ~subst t + with + | None -> args + | Some (_,sats,cpos) -> +(* CSC: sats e' il numero di pi, ma non so cosa farmene! voglio il numero di + argomenti da saltare, come prima! *) + if cpos < List.length args - 1 then + List.nth args (cpos + 1) :: + try snd (HExtlib.split_nth (cpos+sats+2) args) with Failure _->[] + else + args + in + (match args with + [arg] -> idref (k ~context arg) + | _ -> idref (Ast.Appl (List.map (k ~context) args))) | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) -> let name = NUri.name_of_uri uri in (* CSC @@ -242,11 +261,11 @@ let instantiate32 idrefs env symbol args = if args = [] then head else Ast.Appl (head :: List.map instantiate_arg args) -let rec nast_of_cic1 ~idref ~output_type ~subst ~context term = +let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term = match (get_compiled32 ()) term with | None -> - nast_of_cic0 ~idref ~output_type ~subst - (nast_of_cic1 ~idref ~output_type ~subst) ~context term + nast_of_cic0 status ~idref ~output_type ~metasenv ~subst + (nast_of_cic1 status ~idref ~output_type ~metasenv ~subst) ~context term | Some (env, ctors, pid) -> let idrefs = List.map @@ -266,7 +285,8 @@ let rec nast_of_cic1 ~idref ~output_type ~subst ~context term = List.map (fun (name, term) -> name, - nast_of_cic1 ~idref ~output_type ~subst ~context term + nast_of_cic1 status ~idref ~output_type ~subst ~metasenv ~context + term ) env in let _, symbol, args, _ = @@ -387,9 +407,10 @@ let instantiate_appl_pattern aux appl_pattern *) -let nmap_sequent0 ~idref ~subst (i,(n,context,ty):int * NCic.conjecture) = +let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) = let module K = Content in - let nast_of_cic = nast_of_cic1 ~idref ~output_type:`Term ~subst in + let nast_of_cic = + nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in let context',_ = List.fold_right (fun item (res,context) -> @@ -421,11 +442,12 @@ let nmap_sequent0 ~idref ~subst (i,(n,context,ty):int * NCic.conjecture) = ("-1",i,context',nast_of_cic ~context ty) ;; -let nmap_sequent ~subst metasenv = +let nmap_sequent status ~metasenv ~subst conjecture = let module K = Content in let ids_to_refs = Hashtbl.create 211 in let register_ref = Hashtbl.add ids_to_refs in - nmap_sequent0 ~idref:(idref register_ref) ~subst metasenv, ids_to_refs + nmap_sequent0 status ~idref:(idref register_ref) ~metasenv ~subst conjecture, + ids_to_refs ;; let object_prefix = "obj:";; @@ -496,20 +518,20 @@ let build_decl_item seed id n s = } ;; -let nmap_obj (uri,_,metasenv,subst,kind) = +let nmap_obj status (uri,_,metasenv,subst,kind) = let module K = Content in let ids_to_refs = Hashtbl.create 211 in let register_ref = Hashtbl.add ids_to_refs in let idref = idref register_ref in let nast_of_cic = - nast_of_cic1 ~idref ~output_type:`Term ~subst in + nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in let seed = ref 0 in let conjectures = match metasenv with [] -> None | _ -> (*Some (List.map (map_conjectures seed) metasenv)*) (*CSC: used to be the previous line, that uses seed *) - Some (List.map (nmap_sequent0 ~idref ~subst) metasenv) + Some (List.map (nmap_sequent0 status ~idref ~metasenv ~subst) metasenv) in let res = match kind with diff --git a/helm/software/components/ng_cic_content/nTermCicContent.mli b/helm/software/components/ng_cic_content/nTermCicContent.mli index bae7daee2..2a1d7bcc7 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.mli +++ b/helm/software/components/ng_cic_content/nTermCicContent.mli @@ -86,11 +86,12 @@ val nast_of_cic : type id = string val nmap_sequent: - subst:NCic.substitution -> int * NCic.conjecture -> - CicNotationPt.term Content.conjecture * - (id, NReference.reference) Hashtbl.t (* id -> reference *) + #NCicCoercion.status -> metasenv:NCic.metasenv -> subst:NCic.substitution -> + int * NCic.conjecture -> + CicNotationPt.term Content.conjecture * + (id, NReference.reference) Hashtbl.t (* id -> reference *) val nmap_obj: - NCic.obj -> + #NCicCoercion.status -> NCic.obj -> CicNotationPt.term Content.cobj * (id, NReference.reference) Hashtbl.t (* id -> reference *) diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml index 8a6e8a1c8..5e121ccfc 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.ml +++ b/helm/software/components/ng_refiner/nCicCoercion.ml @@ -134,3 +134,31 @@ let look_for_coercion status metasenv subst context infty expty = metasenv, NCicUntrusted.mk_appl t args, ty, List.nth args arg) (CoercionSet.elements candidates) ;; + +(* CSC: very inefficient implementation! + Enrico, can we use a discrimination tree here? *) +let match_coercion status ~metasenv ~subst ~context t = + let db = + DB.fold (fst (status#coerc_db)) (fun _ v l -> (CoercionSet.elements v)@l) [] + in + try + Some + (List.find + (fun (p,_,_) -> + try + let t = + match p,t with + NCic.Appl lp, NCic.Appl lt -> + (match fst (HExtlib.split_nth (List.length lp) lt) with + [t] -> t + | l -> NCic.Appl l) + | _,NCic.Appl (he::_) -> he + | _,_ -> t + in + NCicReduction.alpha_eq metasenv subst context p t + with + Failure _ -> false (* raised by split_nth *) + ) db) + with + Not_found -> None +;; diff --git a/helm/software/components/ng_refiner/nCicCoercion.mli b/helm/software/components/ng_refiner/nCicCoercion.mli index 1d31d469f..ca65aa953 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.mli +++ b/helm/software/components/ng_refiner/nCicCoercion.mli @@ -40,3 +40,8 @@ val look_for_coercion: (* enriched metasenv, new term, its type, metavriable to * be unified with the old term *) (NCic.metasenv * NCic.term * NCic.term * NCic.term) list + +(* returns (coercion,arity,arg) *) +val match_coercion: + #status -> metasenv:NCic.metasenv -> subst:NCic.substitution -> + context:NCic.context -> NCic.term -> (NCic.term * int * int) option diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 5ee48f3da..bdc3b9268 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -66,9 +66,9 @@ let mml_of_cic_sequent metasenv sequent = (asequent, (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts))) -let nmml_of_cic_sequent metasenv subst sequent = +let nmml_of_cic_sequent status metasenv subst sequent = let content_sequent,ids_to_refs = - NTermCicContent.nmap_sequent ~subst sequent in + NTermCicContent.nmap_sequent status ~metasenv ~subst sequent in let pres_sequent = Sequent2pres.nsequent2pres ids_to_refs subst content_sequent in let xmlpres = mpres_document pres_sequent in @@ -90,8 +90,8 @@ let mml_of_cic_object obj = (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses, ids_to_inner_sorts,ids_to_inner_types))) -let nmml_of_cic_object obj = - let cobj,ids_to_nrefs = NTermCicContent.nmap_obj obj in +let nmml_of_cic_object status obj = + let cobj,ids_to_nrefs = NTermCicContent.nmap_obj status obj in let pres_sequent = Content2pres.ncontent2pres ~ids_to_nrefs cobj in let xmlpres = mpres_document pres_sequent in Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres diff --git a/helm/software/matita/applyTransformation.mli b/helm/software/matita/applyTransformation.mli index f41f0a7a1..dbd0343ff 100644 --- a/helm/software/matita/applyTransformation.mli +++ b/helm/software/matita/applyTransformation.mli @@ -45,6 +45,7 @@ val mml_of_cic_sequent: (Cic.id, Cic2acic.sort_kind) Hashtbl.t)) (* ids_to_inner_sorts *) val nmml_of_cic_sequent: + #NCicCoercion.status -> NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *) int * NCic.conjecture -> (* sequent *) Gdome.document (* Math ML *) @@ -60,7 +61,7 @@ val mml_of_cic_object: (Cic.id, Cic2acic.sort_kind) Hashtbl.t * (* ids_to_inner_sorts *) (Cic.id, Cic2acic.anntypes) Hashtbl.t)) (* ids_to_inner_types *) -val nmml_of_cic_object: NCic.obj -> Gdome.document +val nmml_of_cic_object: #NCicCoercion.status -> NCic.obj -> Gdome.document val txt_of_cic_term: map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term -> diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index cd3fe7982..1bfdf8ce3 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -95,7 +95,7 @@ let _ = sequents_viewer#reset; match grafite_status#proof_status with | Incomplete_proof ({ stack = stack } as incomplete_proof) -> - sequents_viewer#load_sequents incomplete_proof; + sequents_viewer#load_sequents grafite_status incomplete_proof; (try script#setGoal (Some (Continuationals.Stack.find_goal stack)); let goal = @@ -103,7 +103,7 @@ let _ = None -> assert false | Some n -> n in - sequents_viewer#goto_sequent goal + sequents_viewer#goto_sequent grafite_status goal with Failure _ -> script#setGoal None); | Proof proof -> sequents_viewer#load_logo_with_qed | No_proof -> @@ -118,7 +118,7 @@ let _ = None -> assert false | Some n -> n in - sequents_viewer#goto_sequent goal + sequents_viewer#goto_sequent grafite_status goal with Failure _ -> script#setGoal None); | `CommandMode -> sequents_viewer#load_logo ) diff --git a/helm/software/matita/matitaGuiTypes.mli b/helm/software/matita/matitaGuiTypes.mli index fb8c1f14a..f2376406a 100644 --- a/helm/software/matita/matitaGuiTypes.mli +++ b/helm/software/matita/matitaGuiTypes.mli @@ -124,10 +124,11 @@ object (** load a sequent and render it into parent widget *) method load_sequent: Cic.metasenv -> int -> unit - method nload_sequent: NCic.metasenv -> NCic.substitution -> int -> unit + method nload_sequent: + #NCicCoercion.status -> NCic.metasenv -> NCic.substitution -> int -> unit method load_object: Cic.obj -> unit - method load_nobject: NCic.obj -> unit + method load_nobject: #NCicCoercion.status -> NCic.obj -> unit end class type sequentsViewer = @@ -135,9 +136,11 @@ object method reset: unit method load_logo: unit method load_logo_with_qed: unit - method load_sequents: GrafiteTypes.incomplete_proof -> unit + method load_sequents: + #NCicCoercion.status -> GrafiteTypes.incomplete_proof -> unit method nload_sequents: #NTacStatus.tac_status -> unit - method goto_sequent: int -> unit (* to be called _after_ load_sequents *) + method goto_sequent: + #NCicCoercion.status -> int -> unit (* to be called _after_ load_sequents *) method cicMathView: cicMathView end diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index f00ea1a0f..255998c4f 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -593,10 +593,14 @@ object (self) end; self#load_root ~root:mathml#get_documentElement - method nload_sequent metasenv subst metano = + method nload_sequent: + 'status. #NCicCoercion.status as 'status -> NCic.metasenv -> + NCic.substitution -> int -> unit + = fun status metasenv subst metano -> let sequent = List.assoc metano metasenv in let mathml = - ApplyTransformation.nmml_of_cic_sequent metasenv subst (metano,sequent) + ApplyTransformation.nmml_of_cic_sequent status metasenv subst + (metano,sequent) in if BuildTimeConf.debug then begin let name = @@ -630,8 +634,10 @@ object (self) self#load_root ~root:mathml#get_documentElement; current_mathml <- Some mathml); - method load_nobject obj = - let mathml = ApplyTransformation.nmml_of_cic_object obj in + method load_nobject : + 'status. #NCicCoercion.status as 'status -> NCic.obj -> unit + = fun status obj -> + let mathml = ApplyTransformation.nmml_of_cic_object status obj in (* self#set_cic_info (Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj)); @@ -718,9 +724,9 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = _metasenv <- `Old []; self#script#setGoal None - method load_sequents - { proof = (_,metasenv,_subst,_,_, _) as proof; stack = stack } - = + method load_sequents : 'status. #NCicCoercion.status as 'status -> 'a + = fun status { proof= (_,metasenv,_subst,_,_, _) as proof; stack = stack } + -> _metasenv <- `Old metasenv; pages <- 0; let win goal_switch = @@ -796,7 +802,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = try List.assoc page page2goal with Not_found -> assert false in self#script#setGoal (Some (goal_of_switch goal_switch)); - self#render_page ~page ~goal_switch)) + self#render_page status ~page ~goal_switch)) method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit = fun status -> @@ -876,14 +882,18 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = try List.assoc page page2goal with Not_found -> assert false in self#script#setGoal (Some (goal_of_switch goal_switch)); - self#render_page ~page ~goal_switch)) + self#render_page status ~page ~goal_switch)) - method private render_page ~page ~goal_switch = + method private render_page: + 'status. #NCicCoercion.status as 'status -> page:int -> + goal_switch:Stack.switch -> unit + = fun status ~page ~goal_switch -> (match goal_switch with | Stack.Open goal -> (match _metasenv with `Old menv -> cicMathView#load_sequent menv goal - | `New (menv,subst) -> cicMathView#nload_sequent menv subst goal) + | `New (menv,subst) -> + cicMathView#nload_sequent status menv subst goal) | Stack.Closed goal -> let doc = Lazy.force closed_goal_mathml in cicMathView#load_root ~root:doc#get_documentElement); @@ -892,7 +902,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = List.assoc goal_switch goal2win () with Not_found -> assert false) - method goto_sequent goal = + method goto_sequent: 'status. #NCicCoercion.status as 'status -> int -> unit + = fun status goal -> let goal_switch, page = try List.find @@ -901,7 +912,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = with Not_found -> assert false in notebook#goto_page page; - self#render_page page goal_switch + self#render_page status ~page ~goal_switch end @@ -1350,7 +1361,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_loadObj obj | _ -> match self#script#grafite_status#ng_mode with - `ProofMode -> self#_loadNObj self#script#grafite_status#obj + `ProofMode -> + self#_loadNObj self#script#grafite_status + self#script#grafite_status#obj | _ -> self#blank () (** loads a cic uri from the environment @@ -1362,7 +1375,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private _loadNReference (NReference.Ref (uri,_)) = let obj = NCicEnvironment.get_checked_obj uri in - self#_loadNObj obj + self#_loadNObj self#script#grafite_status obj method private _loadUnivs uri = let uri = UriManager.strip_xpointer uri in @@ -1404,12 +1417,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_showMath; mathView#load_object obj - method private _loadNObj obj = + method private _loadNObj status obj = (* showMath must be done _before_ loading the document, since if the * widget is not mapped (hidden by the notebook) the document is not * rendered *) self#_showMath; - mathView#load_nobject obj + mathView#load_nobject status obj method private _loadTermCic term metasenv = let context = self#script#proofContext in diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma index f7757ba09..7283cbc58 100644 --- a/helm/software/matita/nlibrary/algebra/magmas.ma +++ b/helm/software/matita/nlibrary/algebra/magmas.ma @@ -75,7 +75,7 @@ ndefinition mm_image: ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism ?? Ma Mb → magma B. #A; #B; #Ma; #Mb; #f; napply (mk_magma ???) - [ napply (image ?? (mmcarr ?? (mmmcarr ???? f)) (mcarr ? Ma)) + [ napply (image ?? (mmcarr ?? (mmmcarr ???? f)) Ma) (* NO COMPOSITE! *) | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd; napply (ex_intro ????) [ napply (op ? x0 y0) -- 2.39.2