aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/mod_subst.ml9
-rw-r--r--kernel/modops.ml31
-rw-r--r--library/declare.ml2
-rw-r--r--library/libnames.ml9
-rw-r--r--library/libnames.mli1
-rw-r--r--pretyping/pattern.ml9
-rw-r--r--tactics/dn.ml14
7 files changed, 46 insertions, 29 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index a9d4a246d..5f81ddb4d 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -596,6 +596,8 @@ let subst_dom_codom_delta_resolver subst resolver =
let update_delta_resolver resolver1 resolver2 =
let apply_res key hint res =
try
+ if Deltamap.mem key resolver2 then
+ res else
match hint with
Prefix_equiv mp ->
let new_hint =
@@ -621,7 +623,7 @@ let add_delta_resolver resolver1 resolver2 =
resolver2
let join (subst1 : substitution) (subst2 : substitution) =
- let apply_subst (sub : substitution) key (mp,resolve) =
+ let apply_subst (sub : substitution) (mp,resolve) =
let mp',resolve' =
match subst_mp0 sub mp with
None -> mp, None
@@ -631,13 +633,12 @@ let join (subst1 : substitution) (subst2 : substitution) =
match resolve' with
Some res ->
add_delta_resolver
- (subst_dom_codom_delta_resolver sub resolve)
- res
+ (subst_dom_codom_delta_resolver sub resolve) res
| None ->
subst_codom_delta_resolver sub resolve
in
mp',resolve'' in
- let subst = Umap.mapi (apply_subst subst2) subst1 in
+ let subst = Umap.map (apply_subst subst2) subst1 in
(Umap.fold Umap.add subst2 subst)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 8193c02e5..7ee48c352 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -126,8 +126,8 @@ and subst_modtype sub do_delta mtb=
let typ_expr' = subst_struct_expr sub do_delta mtb.typ_expr in
let typ_alg' =
Option.smartmap
- (subst_struct_expr sub (fun x -> x)) mtb.typ_expr_alg in
- let mtb_delta = do_delta mtb.typ_delta in
+ (subst_struct_expr sub (fun x y-> x)) mtb.typ_expr_alg in
+ let mtb_delta = do_delta mtb.typ_delta sub in
if typ_expr'==mtb.typ_expr &&
typ_alg'==mtb.typ_expr_alg && mp==mtb.typ_mp then
mtb
@@ -156,7 +156,7 @@ and subst_module sub do_delta mb =
let sub = if is_functor mb.mod_type && not(mp=mb.mod_mp) then
add_mp mb.mod_mp mp
empty_delta_resolver sub else sub in
- let id_delta = (fun x -> x) in
+ let id_delta = (fun x y-> x) in
let mtb',me' =
let mtb = subst_struct_expr sub do_delta mb.mod_type in
match mb.mod_expr with
@@ -168,7 +168,7 @@ and subst_module sub do_delta mb =
in
let typ_alg' = Option.smartmap
(subst_struct_expr sub id_delta) mb.mod_type_alg in
- let mb_delta = do_delta mb.mod_delta in
+ let mb_delta = do_delta mb.mod_delta sub in
if mtb'==mb.mod_type && mb.mod_expr == me'
&& mb_delta == mb.mod_delta && mp == mb.mod_mp
then mb else
@@ -196,11 +196,11 @@ and subst_struct_expr sub do_delta = function
let subst_signature subst =
subst_structure subst
- (fun resolver -> subst_codom_delta_resolver subst resolver)
+ (fun resolver subst-> subst_codom_delta_resolver subst resolver)
let subst_struct_expr subst =
subst_struct_expr subst
- (fun resolver -> subst_codom_delta_resolver subst resolver)
+ (fun resolver subst-> subst_codom_delta_resolver subst resolver)
(* spiwack: here comes the function which takes care of importing
the retroknowledge declared in the library *)
@@ -272,7 +272,6 @@ let strengthen_const env mp_from l cb resolver =
let rec strengthen_mod env mp_from mp_to mb =
- assert(mp_from = mb.mod_mp);
if mp_in_delta mb.mod_mp mb.mod_delta then
mb
else
@@ -385,7 +384,7 @@ let rec strengthen_and_subst_mod
let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in
if mb_is_an_alias then
subst_module subst
- (fun resolver -> subst_dom_delta_resolver subst resolver) mb
+ (fun resolver subst-> subst_dom_delta_resolver subst resolver) mb
else
let resolver,new_sig =
strengthen_and_subst_struct str subst env
@@ -397,8 +396,10 @@ let rec strengthen_and_subst_mod
mod_type = SEBstruct(new_sig);
mod_delta = add_mp_delta_resolver mp_to mp_from resolver}
| SEBfunctor(arg_id,arg_b,body) ->
+ let subst = add_mp mb.mod_mp mp_to empty_delta_resolver subst in
subst_module subst
- (fun resolver -> subst_dom_delta_resolver subst resolver) mb
+ (fun resolver subst-> subst_dom_codom_delta_resolver subst resolver) mb
+
| _ -> anomaly "Modops:the evaluation of the structure failed "
and strengthen_and_subst_struct
@@ -439,7 +440,7 @@ and strengthen_and_subst_struct
let mp_to' = MPdot(mp_to,l) in
let mb_out = if alias then
subst_module subst
- (fun resolver -> subst_dom_delta_resolver subst resolver) mb
+ (fun resolver subst -> subst_dom_delta_resolver subst resolver) mb
else
strengthen_and_subst_mod
mb subst env mp_from' mp_to' env resolver
@@ -449,14 +450,16 @@ and strengthen_and_subst_struct
let resolve_out,rest' =
strengthen_and_subst_struct rest subst env'
mp_alias mp_from mp_to alias incl resolver in
- add_delta_resolver resolve_out mb_out.mod_delta,
+ if is_functor mb_out.mod_type then (add_mp_delta_resolver
+ mp_to' mp_to' resolve_out),item':: rest' else
+ add_delta_resolver resolve_out mb_out.mod_delta,
item':: rest'
| (l,SFBmodtype mty) :: rest ->
let mp_from' = MPdot (mp_from,l) in
let mp_to' = MPdot(mp_to,l) in
let subst' = add_mp mp_from' mp_to' empty_delta_resolver subst in
let mty = subst_modtype subst'
- (fun resolver -> subst_dom_codom_delta_resolver subst' resolver) mty in
+ (fun resolver subst -> subst_dom_codom_delta_resolver subst' resolver) mty in
let env' = add_modtype mp_from' mty env in
let resolve_out,rest' = strengthen_and_subst_struct rest subst env'
mp_alias mp_from mp_to alias incl resolver in
@@ -491,7 +494,7 @@ let strengthen_and_subst_mb mb mp env include_b =
| SEBfunctor(arg_id,argb,body) ->
let subst = map_mp mb.mod_mp mp empty_delta_resolver in
subst_module subst
- (fun resolver -> subst_dom_codom_delta_resolver subst resolver) mb
+ (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mb
| _ -> anomaly "Modops:the evaluation of the structure failed "
@@ -500,4 +503,4 @@ let subst_modtype_and_resolver mtb mp env =
let new_delta = subst_dom_codom_delta_resolver subst mtb.typ_delta in
let full_subst = (map_mp mtb.typ_mp mp new_delta) in
subst_modtype full_subst
- (fun resolver -> subst_dom_codom_delta_resolver subst resolver) mtb
+ (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mtb
diff --git a/library/declare.ml b/library/declare.ml
index 1084aa07d..dd1b12a24 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -163,7 +163,7 @@ let hcons_constant_declaration = function
let declare_constant_common id dhyps (cd,kind) =
let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in
- let c = constant_of_kn kn in
+ let c = Global.constant_of_delta (constant_of_kn kn) in
declare_constant_implicits c;
Heads.declare_head (EvalConstRef c);
Notation.declare_ref_arguments_scope (ConstRef c);
diff --git a/library/libnames.ml b/library/libnames.ml
index fad0336fc..9a7135eae 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -57,6 +57,15 @@ let subst_global subst ref = match ref with
let c',t = subst_constructor subst c in
if c'==c then ref,t else ConstructRef c', t
+let canonical_gr = function
+ | ConstRef con ->
+ ConstRef(constant_of_kn(canonical_con con))
+ | IndRef (kn,i) ->
+ IndRef(mind_of_kn(canonical_mind kn),i)
+ | ConstructRef ((kn,i),j )->
+ ConstructRef((mind_of_kn(canonical_mind kn),i),j)
+ | VarRef id -> VarRef id
+
let global_of_constr c = match kind_of_term c with
| Const sp -> ConstRef sp
| Ind ind_sp -> IndRef ind_sp
diff --git a/library/libnames.mli b/library/libnames.mli
index fd2ca37ae..9ee7d0ab5 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -29,6 +29,7 @@ val isIndRef : global_reference -> bool
val isConstructRef : global_reference -> bool
val eq_gr : global_reference -> global_reference -> bool
+val canonical_gr : global_reference -> global_reference
val destVarRef : global_reference -> variable
val destConstRef : global_reference -> constant
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index ec4a1260c..9acdd1585 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -102,8 +102,8 @@ let rec pattern_of_constr t =
| Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b)
| App (f,a) -> PApp (pattern_of_constr f,Array.map pattern_of_constr a)
| Const sp -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
- | Ind sp -> PRef (IndRef sp)
- | Construct sp -> PRef (ConstructRef sp)
+ | Ind sp -> PRef (canonical_gr (IndRef sp))
+ | Construct sp -> PRef (canonical_gr (ConstructRef sp))
| Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt)
| Case (ci,p,a,br) ->
let cip = ci.ci_pp_info in
@@ -212,9 +212,8 @@ let rec pat_of_raw metas vars = function
with Not_found -> PVar id)
| RPatVar (_,(false,n)) ->
metas := n::!metas; PMeta (Some n)
- | RRef (_,ConstRef con) ->
- PRef (ConstRef (constant_of_kn(canonical_con con)))
- | RRef (_,r) -> PRef r
+ | RRef (_,gr) ->
+ PRef (canonical_gr gr)
(* Hack pour ne pas réécrire une interprétation complète des patterns*)
| RApp (_, RPatVar (_,(true,n)), cl) ->
metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
diff --git a/tactics/dn.ml b/tactics/dn.ml
index 8076e252c..a0889ab8f 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -15,15 +15,19 @@ struct
match x,y with
None,None -> 0
| Some (l,n),Some (l',n') ->
- if (Y.compare l l') = 0 && n = n' then 0
- else Pervasives.compare x y
- | a,b -> Pervasives.compare a b
+ let m = Y.compare l l' in
+ if m = 0 then
+ n-n'
+ else m
+ | Some(l,n),None -> 1
+ | None, Some(l,n) -> -1
end
module X_tries = struct
type t = X.t * Z.t
let compare (x1,x2) (y1,y2) =
- if (X.compare x1 y1) = 0 && (Z.compare x2 y2)=0 then 0
- else Pervasives.compare (x1,x2) (y1,y2)
+ let m = (X.compare x1 y1) in
+ if m = 0 then (Z.compare x2 y2) else
+ m
end
module T = Tries.Make(X_tries)(Y_tries)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 00:20:53 +0000