From 10d33a8c1be31d0c7aeccee8968fd5218ca2510a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 29 Oct 2010 22:29:20 +0000 Subject: [PATCH] More parts of the lexicon status made functional. Still mostly untested. --- .../components/content_pres/content2pres.ml | 5 +- .../components/content_pres/content2pres.mli | 2 +- .../components/content_pres/sequent2pres.ml | 4 +- .../components/content_pres/sequent2pres.mli | 1 + .../content_pres/termContentPres.ml | 125 +++++++++--------- .../content_pres/termContentPres.mli | 29 ++-- matita/components/lexicon/cicNotation.ml | 28 ++-- matita/components/lexicon/cicNotation.mli | 16 ++- matita/components/lexicon/lexiconEngine.ml | 6 +- matita/components/lexicon/lexiconEngine.mli | 4 +- matita/components/statuses.txt | 10 +- matita/matita/applyTransformation.ml | 11 +- matita/matita/applyTransformation.mli | 10 +- matita/matita/matitaGuiTypes.mli | 6 +- matita/matita/matitaMathView.ml | 8 +- matita/matita/nlibrary/depends | 14 +- 16 files changed, 163 insertions(+), 116 deletions(-) diff --git a/matita/components/content_pres/content2pres.ml b/matita/components/content_pres/content2pres.ml index f869801f9..6d8031d85 100644 --- a/matita/components/content_pres/content2pres.ml +++ b/matita/components/content_pres/content2pres.ml @@ -1020,7 +1020,7 @@ let ncontent2pres0 joint.Content.joint_kind joint.Content.joint_defs] | _ -> raise ToDo -let ncontent2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs = +let ncontent2pres status ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs = let lookup_uri id = try let nref = Hashtbl.find ids_to_nrefs id in @@ -1030,4 +1030,5 @@ let ncontent2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs = ncontent2pres0 ?skip_initial_lambdas ?skip_thm_and_qed (fun ?(prec=90) ast -> CicNotationPres.box_of_mpres - (CicNotationPres.render ~lookup_uri ~prec (TermContentPres.pp_ast ast))) + (CicNotationPres.render ~lookup_uri ~prec + (TermContentPres.pp_ast status ast))) diff --git a/matita/components/content_pres/content2pres.mli b/matita/components/content_pres/content2pres.mli index 4b9fc4498..1c5b410b2 100644 --- a/matita/components/content_pres/content2pres.mli +++ b/matita/components/content_pres/content2pres.mli @@ -33,8 +33,8 @@ (**************************************************************************) val ncontent2pres: + #TermContentPres.status -> ?skip_initial_lambdas:int -> ?skip_thm_and_qed:bool -> ids_to_nrefs:(NTermCicContent.id, NReference.reference) Hashtbl.t -> NotationPt.term Content.cobj -> CicNotationPres.boxml_markup - diff --git a/matita/components/content_pres/sequent2pres.ml b/matita/components/content_pres/sequent2pres.ml index 7951dbf5d..53e8e19b4 100644 --- a/matita/components/content_pres/sequent2pres.ml +++ b/matita/components/content_pres/sequent2pres.ml @@ -95,7 +95,7 @@ let sequent2pres0 term2pres (_,_,context,ty) = Box.b_space; pres_goal]))]) -let nsequent2pres ~ids_to_nrefs ~subst = +let nsequent2pres status ~ids_to_nrefs ~subst = let lookup_uri id = try let nref = Hashtbl.find ids_to_nrefs id in @@ -106,4 +106,4 @@ let nsequent2pres ~ids_to_nrefs ~subst = (fun ast -> CicNotationPres.box_of_mpres (CicNotationPres.render ~lookup_uri - (TermContentPres.pp_ast ast))) + (TermContentPres.pp_ast status ast))) diff --git a/matita/components/content_pres/sequent2pres.mli b/matita/components/content_pres/sequent2pres.mli index bf2a30f55..cc3f27457 100644 --- a/matita/components/content_pres/sequent2pres.mli +++ b/matita/components/content_pres/sequent2pres.mli @@ -33,6 +33,7 @@ (***************************************************************************) val nsequent2pres : + #TermContentPres.status -> ids_to_nrefs:(NTermCicContent.id, NReference.reference) Hashtbl.t -> subst:NCic.substitution -> NotationPt.term Content.conjecture -> CicNotationPres.boxml_markup diff --git a/matita/components/content_pres/termContentPres.ml b/matita/components/content_pres/termContentPres.ml index 80d4d65a9..ae4474760 100644 --- a/matita/components/content_pres/termContentPres.ml +++ b/matita/components/content_pres/termContentPres.ml @@ -296,39 +296,45 @@ let pp_ast0 t k = (* persistent state *) -let initial_level1_patterns21 () = Hashtbl.create 211 -let level1_patterns21 = ref (initial_level1_patterns21 ()) -let compiled21 = ref None -let pattern21_matrix = ref [] -let counter = ref ~-1 - -let stack = ref [];; - -let push () = - stack := (!counter,!level1_patterns21,!compiled21,!pattern21_matrix)::!stack; - counter := ~-1; - level1_patterns21 := initial_level1_patterns21 (); - compiled21 := None; - pattern21_matrix := [] -;; - -let pop () = - match !stack with - [] -> assert false - | (ocounter,olevel1_patterns21,ocompiled21,opatterns21_matrix)::old -> - stack := old; - counter := ocounter; - level1_patterns21 := olevel1_patterns21; - compiled21 := ocompiled21; - pattern21_matrix := opatterns21_matrix -;; - -let get_compiled21 () = - match !compiled21 with +module IntMap = Map.Make(struct type t = int let compare = compare end);; + +type db = { + level1_patterns21: NotationPt.term IntMap.t; + compiled21: ((NotationPt.term -> (NotationEnv.t * NotationPt.term list * int) option)) Lazy.t option; + pattern21_matrix: (NotationPt.term * pattern_id) list; + counter: pattern_id +} + +let initial_db = { + level1_patterns21 = IntMap.empty; + compiled21 = None; + pattern21_matrix = []; + counter = ~-1 +} + +class type g_status = + object + method content_pres_db: db + end + +class status = + object + val content_pres_db = initial_db + method content_pres_db = content_pres_db + method set_content_pres_db v = {< content_pres_db = v >} + method set_content_pres_status + : 'status. #g_status as 'status -> 'self + = fun o -> {< content_pres_db = o#content_pres_db >} + end + +let get_compiled21 status = + match status#content_pres_db.compiled21 with | None -> assert false | Some f -> Lazy.force f -let set_compiled21 f = compiled21 := Some f +let set_compiled21 status f = + status#set_content_pres_db + { status#content_pres_db with compiled21 = Some f } let add_idrefs = List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t)) @@ -449,12 +455,12 @@ let instantiate21 idrefs env l1 = in subst_singleton `Left env l1 -let rec pp_ast1 term = +let rec pp_ast1 status term = let rec pp_value = function | NotationEnv.NumValue _ as v -> v | NotationEnv.StringValue _ as v -> v (* | NotationEnv.TermValue t when t == term -> NotationEnv.TermValue (pp_ast0 t pp_ast1) *) - | NotationEnv.TermValue t -> NotationEnv.TermValue (pp_ast1 t) + | NotationEnv.TermValue t -> NotationEnv.TermValue (pp_ast1 status t) | NotationEnv.OptValue None as v -> v | NotationEnv.OptValue (Some v) -> NotationEnv.OptValue (Some (pp_value v)) @@ -467,32 +473,30 @@ let rec pp_ast1 term = (* prerr_endline ("pattern matching from 2 to 1 on term " ^ NotationPp.pp_term term); *) match term with | Ast.AttributedTerm (attrs, term') -> - Ast.AttributedTerm (attrs, pp_ast1 term') + Ast.AttributedTerm (attrs, pp_ast1 status term') | _ -> - (match (get_compiled21 ()) term with - | None -> pp_ast0 term pp_ast1 + (match get_compiled21 status term with + | None -> pp_ast0 term (pp_ast1 status) | Some (env, ctors, pid) -> let idrefs = List.flatten (List.map NotationUtil.get_idrefs ctors) in let l1 = try - Hashtbl.find !level1_patterns21 pid + IntMap.find pid status#content_pres_db.level1_patterns21 with Not_found -> assert false in instantiate21 idrefs (ast_env_of_env env) l1) -let load_patterns21 t = - set_compiled21 (lazy (Content2presMatcher.Matcher21.compiler t)) +let load_patterns21 status t = + set_compiled21 status (lazy (Content2presMatcher.Matcher21.compiler t)) -let pp_ast ast = +let pp_ast status ast = debug_print (lazy "pp_ast <-"); - let ast' = pp_ast1 ast in + let ast' = pp_ast1 status ast in debug_print (lazy ("pp_ast -> " ^ NotationPp.pp_term ast')); ast' -exception Pretty_printer_not_found - let fill_pos_info l1_pattern = l1_pattern (* let rec aux toplevel pos = function @@ -506,26 +510,22 @@ let fill_pos_info l1_pattern = l1_pattern in aux true l1_pattern *) -let fresh_id = - fun () -> - incr counter; - !counter +let fresh_id status = + let counter = status#content_pres_db.counter+1 in + status#set_content_pres_db ({ status#content_pres_db with counter = counter }), counter -let add_pretty_printer l2 (CicNotationParser.CL1P (l1,precedence)) = - let id = fresh_id () in +let add_pretty_printer status l2 (CicNotationParser.CL1P (l1,precedence)) = + let status,id = fresh_id status in let l1' = add_level_info precedence (fill_pos_info l1) in let l2' = NotationUtil.strip_attributes l2 in - Hashtbl.add !level1_patterns21 id l1'; - pattern21_matrix := (l2', id) :: !pattern21_matrix; - load_patterns21 !pattern21_matrix; - id - -let remove_pretty_printer id = - (try - Hashtbl.remove !level1_patterns21 id; - with Not_found -> raise Pretty_printer_not_found); - pattern21_matrix := List.filter (fun (_, id') -> id <> id') !pattern21_matrix; - load_patterns21 !pattern21_matrix + let status = + status#set_content_pres_db + { status#content_pres_db with + level1_patterns21 = + IntMap.add id l1' status#content_pres_db.level1_patterns21; + pattern21_matrix = (l2',id)::status#content_pres_db.pattern21_matrix } in + let status = load_patterns21 status status#content_pres_db.pattern21_matrix in + status,id (* presentation -> content *) @@ -716,10 +716,3 @@ let instantiate_level2 env term = | _ -> assert false in aux env term - - (* initialization *) - -let _ = load_patterns21 [] - - - diff --git a/matita/components/content_pres/termContentPres.mli b/matita/components/content_pres/termContentPres.mli index a9bcd850c..41018d390 100644 --- a/matita/components/content_pres/termContentPres.mli +++ b/matita/components/content_pres/termContentPres.mli @@ -23,23 +23,33 @@ * http://helm.cs.unibo.it/ *) - (** {2 Persistant state handling} *) + (** {2 state handling} *) + +type db + +class type g_status = + object + method content_pres_db: db + end + +class status : + object ('self) + method content_pres_db: db + method set_content_pres_db: db -> 'self + method set_content_pres_status: #g_status -> 'self + end type pretty_printer_id val add_pretty_printer: + #status as 'status -> NotationPt.term -> (* level 2 pattern *) CicNotationParser.checked_l1_pattern -> - pretty_printer_id - -exception Pretty_printer_not_found - - (** @raise Pretty_printer_not_found *) -val remove_pretty_printer: pretty_printer_id -> unit + 'status * pretty_printer_id (** {2 content -> pres} *) -val pp_ast: NotationPt.term -> NotationPt.term +val pp_ast: #status -> NotationPt.term -> NotationPt.term (** {2 pres -> content} *) @@ -47,6 +57,3 @@ val pp_ast: NotationPt.term -> NotationPt.term val instantiate_level2: NotationEnv.t -> NotationPt.term -> NotationPt.term - -val push: unit -> unit -val pop: unit -> unit diff --git a/matita/components/lexicon/cicNotation.ml b/matita/components/lexicon/cicNotation.ml index e25ca3e57..93d8a5570 100644 --- a/matita/components/lexicon/cicNotation.ml +++ b/matita/components/lexicon/cicNotation.ml @@ -32,6 +32,21 @@ type notation_id = | InterpretationId of Interpretations.interpretation_id | PrettyPrinterId of TermContentPres.pretty_printer_id +class type g_status = + object ('self) + inherit Interpretations.g_status + inherit TermContentPres.g_status + end + +class status = + object (self) + inherit Interpretations.status + inherit TermContentPres.status + method set_notation_status + : 'status. #g_status as 'status -> 'self + = fun o -> (self#set_interp_status o)#set_content_pres_status o + end + let compare_notation_id x y = match x,y with | RuleId i1, RuleId i2 -> CicNotationParser.compare_rule_id i1 i2 @@ -67,13 +82,12 @@ let process_notation status st = in RefCounter.incr ~create_cb !parser_ref_counter item in - let pp_id = + let status,pp_id = if dir <> Some `LeftToRight then - [ PrettyPrinterId - (TermContentPres.add_pretty_printer - l2 l1) ] + let status,id = TermContentPres.add_pretty_printer status l2 l1 in + status,[ PrettyPrinterId id ] else - [] + status,[] in status,!rule_id @ pp_id | Interpretation (loc, dsc, l2, l3) -> @@ -91,7 +105,7 @@ let remove_notation = function with Not_found -> assert false in RefCounter.decr ~delete_cb:(fun _ -> CicNotationParser.delete id) !parser_ref_counter item - | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id + | PrettyPrinterId id -> () | InterpretationId id -> () let history = ref [];; @@ -100,12 +114,10 @@ let push () = history := (!parser_ref_counter,!rule_ids_to_items) :: !history; parser_ref_counter := initial_parser_ref_counter (); rule_ids_to_items := initial_rule_ids_to_items (); - TermContentPres.push (); CicNotationParser.push () ;; let pop () = - TermContentPres.pop (); CicNotationParser.pop (); match !history with | [] -> assert false diff --git a/matita/components/lexicon/cicNotation.mli b/matita/components/lexicon/cicNotation.mli index 085feda0d..aa500f371 100644 --- a/matita/components/lexicon/cicNotation.mli +++ b/matita/components/lexicon/cicNotation.mli @@ -25,11 +25,23 @@ type notation_id +class type g_status = + object ('self) + inherit Interpretations.g_status + inherit TermContentPres.g_status + end + +class status : + object ('self) + inherit Interpretations.status + inherit TermContentPres.status + method set_notation_status: #g_status -> 'self + end + val compare_notation_id : notation_id -> notation_id -> int val process_notation: - #Interpretations.status as 'status -> LexiconAst.command - -> 'status * notation_id list + #status as 'status -> LexiconAst.command -> 'status * notation_id list val remove_notation: notation_id -> unit diff --git a/matita/components/lexicon/lexiconEngine.ml b/matita/components/lexicon/lexiconEngine.ml index 4aba86187..7f16fe883 100644 --- a/matita/components/lexicon/lexiconEngine.ml +++ b/matita/components/lexicon/lexiconEngine.ml @@ -49,18 +49,18 @@ let initial_status = { class type g_status = object - inherit Interpretations.g_status + inherit CicNotation.g_status method lstatus: lexicon_status end class status = object(self) - inherit Interpretations.status + inherit CicNotation.status val lstatus = initial_status method lstatus = lstatus method set_lstatus v = {< lstatus = v >} method set_lexicon_engine_status : 'status. #g_status as 'status -> 'self - = fun o -> (self#set_lstatus o#lstatus)#set_interp_status o + = fun o -> (self#set_lstatus o#lstatus)#set_notation_status o end let dump_aliases out msg status = diff --git a/matita/components/lexicon/lexiconEngine.mli b/matita/components/lexicon/lexiconEngine.mli index c4fcac0a8..7e87a22e0 100644 --- a/matita/components/lexicon/lexiconEngine.mli +++ b/matita/components/lexicon/lexiconEngine.mli @@ -34,14 +34,14 @@ type lexicon_status = { class type g_status = object - inherit Interpretations.g_status + inherit CicNotation.g_status method lstatus: lexicon_status end class status : object ('self) inherit g_status - inherit Interpretations.status + inherit CicNotation.status method set_lstatus: lexicon_status -> 'self method set_lexicon_engine_status: #g_status -> 'self end diff --git a/matita/components/statuses.txt b/matita/components/statuses.txt index cb454ba5c..64f41167b 100644 --- a/matita/components/statuses.txt +++ b/matita/components/statuses.txt @@ -1,7 +1,15 @@ grafitetypes -> tac -> auto + eq + (grafitedisambiguate = lexicon+nciccoercion) |--> dumpable | | - |--> nciclibrary interpretation unif_hint + |--> nciclibrary | unif_hint + | + interpretation + termcontentpres = cicnotation + + + + ntermciccontent = nciccoercion+interpretation | unif_hint + +applytransformation = ntermciccontent+termcontentpres diff --git a/matita/matita/applyTransformation.ml b/matita/matita/applyTransformation.ml index f21677e5d..8e09d9db4 100644 --- a/matita/matita/applyTransformation.ml +++ b/matita/matita/applyTransformation.ml @@ -35,6 +35,13 @@ (* $Id$ *) +class status = + object + inherit NTermCicContent.status + inherit TermContentPres.status + end + + let mpres_document pres_box = Xml.add_xml_declaration (CicNotationPres.print_box pres_box) @@ -42,14 +49,14 @@ let ntxt_of_cic_sequent ~map_unicode_to_tex size status metasenv subst sequent = let content_sequent,ids_to_refs = NTermCicContent.nmap_sequent status ~metasenv ~subst sequent in let pres_sequent = - Sequent2pres.nsequent2pres ids_to_refs subst content_sequent in + Sequent2pres.nsequent2pres status ids_to_refs subst content_sequent in let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in BoxPp.render_to_string ~map_unicode_to_tex (function x::_ -> x | _ -> assert false) size pres_sequent let ntxt_of_cic_object ~map_unicode_to_tex size status obj = let cobj,ids_to_nrefs = NTermCicContent.nmap_obj status obj in - let pres_sequent = Content2pres.ncontent2pres ~ids_to_nrefs cobj in + let pres_sequent = Content2pres.ncontent2pres status ~ids_to_nrefs cobj in let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in BoxPp.render_to_string ~map_unicode_to_tex (function x::_ -> x | _ -> assert false) size pres_sequent diff --git a/matita/matita/applyTransformation.mli b/matita/matita/applyTransformation.mli index e67a88ee3..6d3e40810 100644 --- a/matita/matita/applyTransformation.mli +++ b/matita/matita/applyTransformation.mli @@ -33,12 +33,18 @@ (* *) (***************************************************************************) +class status : + object ('self) + inherit NTermCicContent.status + inherit TermContentPres.status + end + val ntxt_of_cic_sequent: map_unicode_to_tex:bool -> int -> - #NTermCicContent.status -> + #status -> NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *) int * NCic.conjecture -> (* sequent *) string (* text *) val ntxt_of_cic_object: - map_unicode_to_tex:bool -> int -> #NTermCicContent.status -> NCic.obj -> string + map_unicode_to_tex:bool -> int -> #status -> NCic.obj -> string diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli index 64dd3cd6f..ddd08caf6 100644 --- a/matita/matita/matitaGuiTypes.mli +++ b/matita/matita/matitaGuiTypes.mli @@ -131,9 +131,9 @@ object (** load a sequent and render it into parent widget *) method nload_sequent: - #NTermCicContent.status -> NCic.metasenv -> NCic.substitution -> int -> unit + #ApplyTransformation.status -> NCic.metasenv -> NCic.substitution -> int -> unit - method load_nobject: #NTermCicContent.status -> NCic.obj -> unit + method load_nobject: #ApplyTransformation.status -> NCic.obj -> unit end class type sequentsViewer = @@ -143,7 +143,7 @@ object method load_logo_with_qed: unit method nload_sequents: #NTacStatus.tac_status -> unit method goto_sequent: - #NTermCicContent.status -> int -> unit (* to be called _after_ load_sequents *) + #ApplyTransformation.status -> int -> unit (* to be called _after_ load_sequents *) method cicMathView: cicMathView end diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index d0710ab4e..78e0a13a5 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -620,7 +620,7 @@ object (self) val mutable current_mathml = None method nload_sequent: - 'status. #NTermCicContent.status as 'status -> NCic.metasenv -> + 'status. #ApplyTransformation.status as 'status -> NCic.metasenv -> NCic.substitution -> int -> unit = fun status metasenv subst metano -> let sequent = List.assoc metano metasenv in @@ -637,7 +637,7 @@ object (self) self#load_root ~root:txt method load_nobject : - 'status. #NTermCicContent.status as 'status -> NCic.obj -> unit + 'status. #ApplyTransformation.status as 'status -> NCic.obj -> unit = fun status obj -> let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false 80 status obj in @@ -808,7 +808,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = self#render_page status ~page ~goal_switch)) method private render_page: - 'status. #NTermCicContent.status as 'status -> page:int -> + 'status. #ApplyTransformation.status as 'status -> page:int -> goal_switch:Stack.switch -> unit = fun status ~page ~goal_switch -> (match goal_switch with @@ -825,7 +825,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = List.assoc goal_switch goal2win () with Not_found -> assert false) - method goto_sequent: 'status. #NTermCicContent.status as 'status -> int -> unit + method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit = fun status goal -> let goal_switch, page = try diff --git a/matita/matita/nlibrary/depends b/matita/matita/nlibrary/depends index 96eca527f..67c9906cf 100644 --- a/matita/matita/nlibrary/depends +++ b/matita/matita/nlibrary/depends @@ -1,6 +1,5 @@ -.unnamed.ma datatypes/list.ma sets/setoids.ma -PTS/subst.ma basics/list2.ma topology/igft3.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma +PTS/subst.ma basics/list2.ma basics/functions.ma Plogic/connectives.ma Plogic/equality.ma nat/compare.ma datatypes/bool.ma nat/order.ma arithmetics/compare.ma arithmetics/nat.ma @@ -32,32 +31,33 @@ sets/categories2.ma sets/categories.ma sets/setoids2.ma sets/sets.ma basics/list2.ma arithmetics/nat.ma basics/list.ma arithmetics/nat.ma basics/bool.ma basics/eq.ma basics/functions.ma hints_declaration.ma sets/setoids1.ma hints_declaration.ma properties/relations1.ma sets/setoids.ma +B.ma A.ma nat/minus.ma nat/order.ma logic/cologic.ma Plogic/connectives.ma Plogic/equality.ma datatypes/bool.ma logic/equality.ma logic/pts.ma -SET171^3.ma TPTP.ma datatypes/list.ma logic/pts.ma Plogic/jmeq.ma Plogic/equality.ma sets/partitions.ma datatypes/pairs.ma nat/compare.ma nat/minus.ma nat/plus.ma sets/sets.ma topology/igft-setoid.ma sets/sets.ma sets/setoids.ma hints_declaration.ma logic/connectives.ma properties/relations.ma properties/relations.ma logic/pts.ma -nat/big_ops.ma algebra/magmas.ma nat/order.ma +nat/big_ops.ma algebra/magmas.ma logic/equality.ma nat/order.ma arithmetics/R.ma arithmetics/nat.ma datatypes/pairs.ma datatypes/sums.ma topology/igft.ma arithmetics/minimization.ma arithmetics/nat.ma algebra/unital_magmas.ma algebra/magmas.ma properties/relations1.ma logic/pts.ma basics/bool.ma basics/eq.ma basics/functions.ma -datatypes/bool-setoids.ma datatypes/bool.ma sets/setoids.ma -logic/equality.ma logic/connectives.ma properties/relations.ma +datatypes/bool-setoids.ma datatypes/bool.ma properties/relations.ma sets/setoids.ma datatypes/pairs-setoids.ma datatypes/pairs.ma sets/setoids.ma +logic/equality.ma logic/connectives.ma properties/relations.ma topology/igft4.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma basics/eq.ma basics/relations.ma datatypes/sums.ma datatypes/pairs.ma hints_declaration.ma logic/pts.ma +A.ma logic/pts.ma logic/destruct_bb.ma logic/equality.ma topology/igft.ma logic/equality.ma sets/sets.ma -algebra/abelian_magmas.ma algebra/magmas.ma overlap/o-algebra.ma sets/categories2.ma +algebra/abelian_magmas.ma algebra/magmas.ma re/re.ma arithmetics/nat.ma datatypes/list.ma datatypes/pairs.ma hints_declaration.ma basics/list.ma basics/bool.ma basics/eq.ma nat/nat.ma hints_declaration.ma logic/equality.ma sets/setoids.ma -- 2.39.2