From ec13ac23f555f04b0a546d0e8ae464d9b5806d9b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 27 Jan 2006 17:32:35 +0000 Subject: [PATCH] 1. The last commit that fixed unification of compound coercions with applied atomic coercions used to introduce too many compound coercions at the end. In this commit we fix the problem in a brutal way by mergin coercions every time CicMetaSubst.apply_subst is called. To be refined later on. 2. Several bug fixed in coercions handling. In particular, a coercion whose source or target was a name was given an invalid URI and was not unified and applied correctly. 3. New version of the algebraic library. In this version we differentiate between pre-structures and structures. This allows a few theorems/lemmas to be stated in a more natural way. --- helm/matita/library/algebra/groups.ma | 79 ++++++++------ helm/matita/library/algebra/monoids.ma | 58 +++++----- helm/matita/library/algebra/semigroups.ma | 42 ++++---- helm/ocaml/cic_unification/cicMetaSubst.ml | 2 +- helm/ocaml/cic_unification/cicRefine.ml | 22 +++- helm/ocaml/cic_unification/cicUnification.ml | 5 +- helm/ocaml/library/coercDb.ml | 18 ++-- helm/ocaml/library/librarySync.ml | 107 ++++++++++--------- helm/ocaml/library/librarySync.mli | 2 + 9 files changed, 192 insertions(+), 143 deletions(-) diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma index bec57fb4c..ae6b525e3 100644 --- a/helm/matita/library/algebra/groups.ma +++ b/helm/matita/library/algebra/groups.ma @@ -17,24 +17,27 @@ set "baseuri" "cic:/matita/algebra/groups/". include "algebra/monoids.ma". include "nat/le_arith.ma". -record isGroup (M:Monoid) (opp: M -> M) : Prop ≝ - { opp_is_left_inverse: is_left_inverse M opp; - opp_is_right_inverse: is_right_inverse M opp +record PreGroup : Type ≝ + { premonoid:> PreMonoid; + opp: premonoid -> premonoid + }. + +record isGroup (G:PreGroup) : Prop ≝ + { is_monoid: isMonoid G; + opp_is_left_inverse: is_left_inverse (mk_Monoid ? is_monoid) (opp G); + opp_is_right_inverse: is_right_inverse (mk_Monoid ? is_monoid) (opp G) }. record Group : Type ≝ - { monoid: Monoid; - opp: monoid -> monoid; - group_properties: isGroup ? opp + { pregroup:> PreGroup; + group_properties:> isGroup pregroup }. -coercion cic:/matita/algebra/groups/monoid.con. - -notation < "G" +(*notation < "G" for @{ 'monoid $G }. interpretation "Monoid coercion" 'monoid G = - (cic:/matita/algebra/groups/monoid.con G). + (cic:/matita/algebra/groups/monoid.con G).*) notation < "G" for @{ 'type_of_group $G }. @@ -43,10 +46,10 @@ interpretation "Type_of_group coercion" 'type_of_group G = (cic:/matita/algebra/groups/Type_of_Group.con G). notation < "G" -for @{ 'semigroup_of_group $G }. +for @{ 'magma_of_group $G }. -interpretation "Semigroup_of_group coercion" 'semigroup_of_group G = - (cic:/matita/algebra/groups/SemiGroup_of_Group.con G). +interpretation "magma_of_group coercion" 'magma_of_group G = + (cic:/matita/algebra/groups/Magma_of_Group.con G). notation "hvbox(x \sup (-1))" with precedence 89 for @{ 'gopp $x }. @@ -68,11 +71,11 @@ intros; unfold left_cancellable; unfold injective; intros (x y z); -rewrite < (e_is_left_unit ? ? (monoid_properties G)); -rewrite < (e_is_left_unit ? ? (monoid_properties G) z); -rewrite < (opp_is_left_inverse ? ? (group_properties G) x); -rewrite > (semigroup_properties G); -rewrite > (semigroup_properties G); +rewrite < (e_is_left_unit ? (is_monoid ? (group_properties G))); +rewrite < (e_is_left_unit ? (is_monoid ? (group_properties G)) z); +rewrite < (opp_is_left_inverse ? (group_properties G) x); +rewrite > (associative ? (is_semi_group ? (is_monoid ? (group_properties G)))); +rewrite > (associative ? (is_semi_group ? (is_monoid ? (group_properties G)))); apply eq_f; assumption. qed. @@ -85,11 +88,11 @@ unfold right_cancellable; unfold injective; simplify;fold simplify (op G); intros (x y z); -rewrite < (e_is_right_unit ? ? (monoid_properties G)); -rewrite < (e_is_right_unit ? ? (monoid_properties G) z); -rewrite < (opp_is_right_inverse ? ? (group_properties G) x); -rewrite < (semigroup_properties G); -rewrite < (semigroup_properties G); +rewrite < (e_is_right_unit ? (is_monoid ? (group_properties G))); +rewrite < (e_is_right_unit ? (is_monoid ? (group_properties G)) z); +rewrite < (opp_is_right_inverse ? (group_properties G) x); +rewrite < (associative ? (is_semi_group ? (is_monoid ? (group_properties G)))); +rewrite < (associative ? (is_semi_group ? (is_monoid ? (group_properties G)))); rewrite > H; reflexivity. qed. @@ -119,13 +122,10 @@ interpretation "Finite_enumerable order" 'card C = (cic:/matita/algebra/groups/order.con C _). record finite_enumerable_SemiGroup : Type ≝ - { semigroup: SemiGroup; - is_finite_enumerable: finite_enumerable semigroup + { semigroup:> SemiGroup; + is_finite_enumerable:> finite_enumerable semigroup }. -coercion cic:/matita/algebra/groups/semigroup.con. -coercion cic:/matita/algebra/groups/is_finite_enumerable.con. - notation < "S" for @{ 'semigroup_of_finite_enumerable_semigroup $S }. @@ -134,6 +134,14 @@ interpretation "Semigroup_of_finite_enumerable_semigroup" = (cic:/matita/algebra/groups/semigroup.con S). +notation < "S" +for @{ 'magma_of_finite_enumerable_semigroup $S }. + +interpretation "Magma_of_finite_enumerable_semigroup" + 'magma_of_finite_enumerable_semigroup S += + (cic:/matita/algebra/groups/Magma_of_finite_enumerable_SemiGroup.con S). + notation < "S" for @{ 'type_of_finite_enumerable_semigroup $S }. @@ -159,7 +167,7 @@ theorem foo: ∀G:finite_enumerable_SemiGroup. left_cancellable ? (op G) → right_cancellable ? (op G) → - ∃e:G. isMonoid G e. + ∃e:G. isMonoid (mk_PreMonoid G e). intros; letin f ≝ (λn.ι(G \sub O · G \sub n)); cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n); @@ -178,23 +186,26 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n); clearbody GOGO; rewrite < HH in GOGO; rewrite < HH in GOGO:(? ? % ?); - rewrite > (semigroup_properties G) in GOGO; + rewrite > (associative ? G) in GOGO; letin GaGa ≝ (H ? ? ? GOGO); clearbody GaGa; clear GOGO; constructor 1; - [ unfold is_left_unit; intro; + [ simplify; + apply (semigroup_properties G) + | unfold is_left_unit; intro; letin GaxGax ≝ (refl_eq ? (G \sub a ·x)); clearbody GaxGax; rewrite < GaGa in GaxGax:(? ? % ?); - rewrite > (semigroup_properties G) in GaxGax; + rewrite > (associative ? (semigroup_properties G)) in GaxGax; apply (H ? ? ? GaxGax) | unfold is_right_unit; intro; letin GaxGax ≝ (refl_eq ? (x·G \sub a)); clearbody GaxGax; rewrite < GaGa in GaxGax:(? ? % ?); - rewrite < (semigroup_properties G) in GaxGax; + rewrite < (associative ? (semigroup_properties G)) in GaxGax; apply (H1 ? ? ? GaxGax) + ] ] | -]. \ No newline at end of file +]. diff --git a/helm/matita/library/algebra/monoids.ma b/helm/matita/library/algebra/monoids.ma index cf1e531f4..c3f3cc48e 100644 --- a/helm/matita/library/algebra/monoids.ma +++ b/helm/matita/library/algebra/monoids.ma @@ -16,38 +16,46 @@ set "baseuri" "cic:/matita/algebra/monoids/". include "algebra/semigroups.ma". -record isMonoid (SS:SemiGroup) (e:SS) : Prop ≝ - { e_is_left_unit: is_left_unit SS e; - e_is_right_unit: is_right_unit SS e +record PreMonoid : Type ≝ + { magma:> Magma; + e: magma + }. + +notation < "M" for @{ 'pmmagma $M }. +interpretation "premonoid magma coercion" 'pmmagma M = + (cic:/matita/algebra/monoids/magma.con M). + +record isMonoid (M:PreMonoid) : Prop ≝ + { is_semi_group: isSemiGroup M; + e_is_left_unit: + is_left_unit (mk_SemiGroup ? is_semi_group) (e M); + e_is_right_unit: + is_right_unit (mk_SemiGroup ? is_semi_group) (e M) }. record Monoid : Type ≝ - { semigroup: SemiGroup; - e: semigroup; - monoid_properties: isMonoid ? e + { premonoid:> PreMonoid; + monoid_properties:> isMonoid premonoid }. - -coercion cic:/matita/algebra/monoids/semigroup.con. - -(* too ugly -notation "hvbox(1 \sub S)" with precedence 89 -for @{ 'munit $S }. - -interpretation "Monoid unit" 'munit S = - (cic:/matita/algebra/monoids/e.con S). *) +notation < "M" for @{ 'semigroup $M }. +interpretation "premonoid coercion" 'premonoid M = + (cic:/matita/algebra/monoids/premonoid.con M). + +notation < "M" for @{ 'typeofmonoid $M }. +interpretation "premonoid coercion" 'typeofmonoid M = + (cic:/matita/algebra/monoids/Type_of_Monoid.con M). + +notation < "M" for @{ 'magmaofmonoid $M }. +interpretation "premonoid coercion" 'magmaofmonoid M = + (cic:/matita/algebra/monoids/Magma_of_Monoid.con M). + notation "1" with precedence 89 for @{ 'munit }. interpretation "Monoid unit" 'munit = (cic:/matita/algebra/monoids/e.con _). -notation < "M" -for @{ 'semigroup $M }. - -interpretation "Semigroup coercion" 'semigroup M = - (cic:/matita/algebra/monoids/semigroup.con M). - definition is_left_inverse ≝ λM:Monoid. λopp: M → M. @@ -67,13 +75,11 @@ theorem is_left_inverse_to_is_right_inverse_to_eq: generalize in match (eq_f ? ? (λy.y·(r x)) ? ? H2); simplify; fold simplify (op M); intro; clear H2; - generalize in match (semigroup_properties M); - fold simplify (Type_of_Monoid M); + generalize in match (associative ? (is_semi_group ? (monoid_properties M))); intro; - unfold isSemiGroup in H2; unfold associative in H2; rewrite > H2 in H3; clear H2; rewrite > H1 in H3; - rewrite > (e_is_left_unit ? ? (monoid_properties M)) in H3; - rewrite > (e_is_right_unit ? ? (monoid_properties M)) in H3; + rewrite > (e_is_left_unit ? (monoid_properties M)) in H3; + rewrite > (e_is_right_unit ? (monoid_properties M)) in H3; assumption. qed. diff --git a/helm/matita/library/algebra/semigroups.ma b/helm/matita/library/algebra/semigroups.ma index d41c416f8..5b461d1a4 100644 --- a/helm/matita/library/algebra/semigroups.ma +++ b/helm/matita/library/algebra/semigroups.ma @@ -16,38 +16,38 @@ set "baseuri" "cic:/matita/algebra/semigroups". include "higher_order_defs/functions.ma". -definition isSemiGroup ≝ - λC:Type. λop: C → C → C.associative C op. +(* Magmas *) -record SemiGroup : Type ≝ - { carrier: Type; - op: carrier → carrier → carrier; - semigroup_properties: isSemiGroup carrier op +record Magma : Type ≝ + { carrier:> Type; + op: carrier → carrier → carrier }. - -coercion cic:/matita/algebra/semigroups/carrier.con. -notation "hvbox(a break \middot \sub S b)" - left associative with precedence 55 -for @{ 'ptimes $S $a $b }. +notation < "M" for @{ 'carrier $M }. +interpretation "carrier coercion" 'carrier S = + (cic:/matita/algebra/semigroups/carrier.con S). notation "hvbox(a break \middot b)" left associative with precedence 55 -for @{ 'ptimesi $a $b }. +for @{ 'magma_op $a $b }. -interpretation "Semigroup operation" 'ptimesi a b = +interpretation "magma operation" 'magma_op a b = (cic:/matita/algebra/semigroups/op.con _ a b). -(* too ugly -interpretation "Semigroup operation" 'ptimes S a b = - (cic:/matita/algebra/semigroups/op.con S a b). *) - -notation < "S" -for @{ 'carrier $S }. +(* Semigroups *) -interpretation "Carrier coercion" 'carrier S = - (cic:/matita/algebra/semigroups/carrier.con S). +record isSemiGroup (M:Magma) : Prop ≝ + { associative: associative ? (op M) }. +record SemiGroup : Type ≝ + { magma:> Magma; + semigroup_properties:> isSemiGroup magma + }. + +notation < "S" for @{ 'magma $S }. +interpretation "magma coercion" 'magma S = + (cic:/matita/algebra/semigroups/magma.con S). + definition is_left_unit ≝ λS:SemiGroup. λe:S. ∀x:S. e·x = x. diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index afd74d756..5870089be 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -230,7 +230,7 @@ let apply_subst_gen ~appl_fun subst term = in C.CoFix (i, fl') in - um_aux term + LibrarySync.merge_coercions (um_aux term) ;; let apply_subst = diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 1caeb733d..620f66f18 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -1115,9 +1115,25 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let newt, _, subst, metasenv, ugraph = avoid_double_coercion subst metasenv ugraph - (Cic.Appl[c;hete]) tgt_carr - in - newt, subst, metasenv, ugraph) + (Cic.Appl[c;hete]) tgt_carr in + try + let newty,newhety,subst,metasenv,ugraph = + type_of_aux subst metasenv context newt ugraph in + let subst,metasenv,ugraph1 = + fo_unif_subst subst context metasenv + newhety s ugraph + in + newt, subst, metasenv, ugraph + with exn -> + enrich localization_tbl hete + ~f:(fun _ -> + (lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst hete + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst hety + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst s context + (* "\nReason: " ^ Lazy.force e*)))) exn) | exn -> enrich localization_tbl hete ~f:(fun _ -> diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 8deb6af4a..d1e010ca6 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -575,7 +575,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ fo_unif_l test_equality_only subst metasenv (lr1, lr2) ugraph with - | UnificationFailure _ as exn -> + | UnificationFailure _ + | Uncertain _ as exn -> (match l1, l2 with | (((Cic.Const (uri1, ens1)) as c1) :: tl1), (((Cic.Const (uri2, ens2)) as c2) :: tl2) when @@ -583,7 +584,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ CoercGraph.is_a_coercion c2 -> let body1, attrs1, ugraph = match CicEnvironment.get_obj ugraph uri1 with - | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u + | Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u | _ -> assert false in let body2, attrs2, ugraph = diff --git a/helm/ocaml/library/coercDb.ml b/helm/ocaml/library/coercDb.ml index 01065325f..8e2c62f31 100644 --- a/helm/ocaml/library/coercDb.ml +++ b/helm/ocaml/library/coercDb.ml @@ -37,9 +37,21 @@ let coerc_carr_of_term t = with Invalid_argument _ -> match t with | Cic.Sort s -> Sort s + | Cic.Appl ((Cic.Const (uri, _))::_) + | Cic.Appl ((Cic.MutInd (uri, _, _))::_) + | Cic.Appl ((Cic.MutConstruct (uri, _, _, _))::_) -> Uri uri | t -> Term t ;; +let name_of_carr = function + | Uri u -> UriManager.name_of_uri u + | Sort s -> CicPp.ppsort s + | Term (Cic.Appl ((Cic.Const (uri, _))::_)) + | Term (Cic.Appl ((Cic.MutInd (uri, _, _))::_)) + | Term (Cic.Appl ((Cic.MutConstruct (uri, _, _, _))::_)) -> + UriManager.name_of_uri uri + | Term t -> (* CicPp.ppterm t *) assert false + let eq_carr src tgt = match src, tgt with | Uri src, Uri tgt -> UriManager.eq src tgt @@ -54,12 +66,6 @@ let eq_carr src tgt = else raise EqCarrOnNonMetaClosed | _, _ -> false -let name_of_carr = function - | Uri u -> UriManager.name_of_uri u - | Sort s -> CicPp.ppsort s - | Term t -> CicPp.ppterm t - - let to_list () = !db diff --git a/helm/ocaml/library/librarySync.ml b/helm/ocaml/library/librarySync.ml index 92926464b..7363697d5 100644 --- a/helm/ocaml/library/librarySync.ml +++ b/helm/ocaml/library/librarySync.ml @@ -37,66 +37,73 @@ let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29 * *) let coercion_hashtbl = UriManager.UriHashtbl.create 3 -let merge_coercions obj = +let rec merge_coercions = + let module C = Cic in + let aux = (fun (u,t) -> u,merge_coercions t) in + function + C.Rel _ | C.Sort _ | C.Implicit _ as t -> t + | C.Meta (n,subst) -> + let subst' = + List.map + (function None -> None | Some t -> Some (merge_coercions t)) subst + in + C.Meta (n,subst') + | C.Cast (te,ty) -> C.Cast (merge_coercions te, merge_coercions ty) + | C.Prod (name,so,dest) -> + C.Prod (name, merge_coercions so, merge_coercions dest) + | C.Lambda (name,so,dest) -> + C.Lambda (name, merge_coercions so, merge_coercions dest) + | C.LetIn (name,so,dest) -> + C.LetIn (name, merge_coercions so, merge_coercions dest) + | Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ] when + CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 -> + let source_carr = CoercGraph.source_of c2 in + let tgt_carr = CoercGraph.target_of c1 in + (match CoercGraph.look_for_coercion source_carr tgt_carr + with + | CoercGraph.SomeCoercion c -> Cic.Appl [ c ; head ] + | _ -> assert false) (* the composite coercion must exist *) + | C.Appl l -> C.Appl (List.map merge_coercions l) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst = List.map aux exp_named_subst in + C.Var (uri, exp_named_subst) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst = List.map aux exp_named_subst in + C.Const (uri, exp_named_subst) + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst = List.map aux exp_named_subst in + C.MutInd (uri,tyno,exp_named_subst) + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst = List.map aux exp_named_subst in + C.MutConstruct (uri,tyno,consno,exp_named_subst) + | C.MutCase (uri,tyno,out,te,pl) -> + let pl = List.map merge_coercions pl in + C.MutCase (uri,tyno,merge_coercions out,merge_coercions te,pl) + | C.Fix (fno, fl) -> + let fl = List.map (fun (name,idx,ty,bo)->(name,idx,merge_coercions ty,merge_coercions bo)) fl in + C.Fix (fno, fl) + | C.CoFix (fno, fl) -> + let fl = List.map (fun (name,ty,bo) -> (name, merge_coercions ty, merge_coercions bo)) fl in + C.CoFix (fno, fl) + +let merge_coercions_in_obj obj = let module C = Cic in - let rec aux2 = (fun (u,t) -> u,aux t) - and aux = function - | C.Rel _ | C.Sort _ as t -> t - | C.Meta _ | C.Implicit _ -> assert false - | C.Cast (te,ty) -> C.Cast (aux te, aux ty) - | C.Prod (name,so,dest) -> - C.Prod (name, aux so, aux dest) - | C.Lambda (name,so,dest) -> - C.Lambda (name, aux so, aux dest) - | C.LetIn (name,so,dest) -> - C.LetIn (name, aux so, aux dest) - | Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ] when - CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 -> - let source_carr = CoercGraph.source_of c2 in - let tgt_carr = CoercGraph.target_of c1 in - (match CoercGraph.look_for_coercion source_carr tgt_carr - with - | CoercGraph.SomeCoercion c -> Cic.Appl [ c ; head ] - | _ -> assert false) (* the composite coercion must exist *) - | C.Appl l -> C.Appl (List.map aux l) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst = List.map aux2 exp_named_subst in - C.Var (uri, exp_named_subst) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst = List.map aux2 exp_named_subst in - C.Const (uri, exp_named_subst) - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst = List.map aux2 exp_named_subst in - C.MutInd (uri,tyno,exp_named_subst) - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst = List.map aux2 exp_named_subst in - C.MutConstruct (uri,tyno,consno,exp_named_subst) - | C.MutCase (uri,tyno,out,te,pl) -> - let pl = List.map aux pl in - C.MutCase (uri,tyno,aux out,aux te,pl) - | C.Fix (fno, fl) -> - let fl = List.map (fun (name,idx,ty,bo)->(name,idx,aux ty,aux bo)) fl in - C.Fix (fno, fl) - | C.CoFix (fno, fl) -> - let fl = List.map (fun (name,ty,bo) -> (name, aux ty, aux bo)) fl in - C.CoFix (fno, fl) - in match obj with | C.Constant (id, body, ty, params, attrs) -> let body = match body with | None -> None - | Some body -> Some (aux body) + | Some body -> Some (merge_coercions body) in - let ty = aux ty in + let ty = merge_coercions ty in C.Constant (id, body, ty, params, attrs) | C.Variable (name, body, ty, params, attrs) -> let body = match body with | None -> None - | Some body -> Some (aux body) + | Some body -> Some (merge_coercions body) in - let ty = aux ty in + let ty = merge_coercions ty in C.Variable (name, body, ty, params, attrs) | C.CurrentProof (_name, _conjectures, _body, _ty, _params, _attrs) -> assert false @@ -104,8 +111,8 @@ let merge_coercions obj = let indtys = List.map (fun (name, ind, arity, cl) -> - let arity = aux arity in - let cl = List.map (fun (name, ty) -> (name,aux ty)) cl in + let arity = merge_coercions arity in + let cl = List.map (fun (name, ty) -> (name,merge_coercions ty)) cl in (name, ind, arity, cl)) indtys in @@ -183,7 +190,7 @@ let add_single_obj uri obj ~basedir = if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*) not (CoercGraph.is_a_coercion (Cic.Const (uri, []))) then - merge_coercions obj + merge_coercions_in_obj obj else obj in diff --git a/helm/ocaml/library/librarySync.mli b/helm/ocaml/library/librarySync.mli index 43ac34da3..d063b3282 100644 --- a/helm/ocaml/library/librarySync.mli +++ b/helm/ocaml/library/librarySync.mli @@ -25,6 +25,8 @@ exception AlreadyDefined of UriManager.uri +val merge_coercions: Cic.term -> Cic.term + (* adds an object to the library together with all auxiliary lemmas on it *) (* (e.g. elimination principles, projections, etc.) *) (* it returns the list of the uris of the auxiliary lemmas generated *) -- 2.39.2