diff options
| -rw-r--r-- | doc/stdlib/index-list.html.template | 3 | ||||
| -rw-r--r-- | kernel/constr.ml | 27 | ||||
| -rw-r--r-- | kernel/univ.ml | 33 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 20 |
4 files changed, 53 insertions, 30 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 1f8ff94e1..d774ed597 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -393,6 +393,9 @@ through the <tt>Require Import</tt> command.</p> theories/Classes/Morphisms_Prop.v theories/Classes/Morphisms_Relations.v theories/Classes/Equivalence.v + theories/Classes/CRelationClasses.v + theories/Classes/CMorphisms.v + theories/Classes/CEquivalence.v theories/Classes/EquivDec.v theories/Classes/SetoidTactics.v theories/Classes/SetoidClass.v diff --git a/kernel/constr.ml b/kernel/constr.ml index ac2c4418e..271691e02 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -723,8 +723,8 @@ let hasheq t1 t2 = | Lambda (n1,t1,c1), Lambda (n2,t2,c2) -> n1 == n2 && t1 == t2 && c1 == c2 | LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) -> n1 == n2 && b1 == b2 && t1 == t2 && c1 == c2 - | Proj (c1,t1), Proj (c2,t2) -> c1 == c2 && t1 == t2 | App (c1,l1), App (c2,l2) -> c1 == c2 && array_eqeq l1 l2 + | Proj (p1,c1), Proj(p2,c2) -> p1 == p2 && c1 == c2 | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && array_eqeq l1 l2 | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2 | Ind ((sp1,i1),u1), Ind ((sp2,i2),u2) -> @@ -807,8 +807,8 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = (Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl)) | Proj (p,c) -> let c, hc = sh_rec c in - let p' = sh_con p in - (Proj (p', c), combinesmall 17 (Hashtbl.hash p')) + let p' = sh_con p in + (Proj (p', c), combinesmall 17 (combine (Constant.hash p') hc)) | Const (c,u) -> let c' = sh_con c in let u', hu = sh_instance u in @@ -973,9 +973,24 @@ module Hsorts = let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate hcons_ind -let hcons_pconstruct (c,u) = (hcons_construct c, Univ.Instance.hcons u) -let hcons_pind (i,u) = (hcons_ind i, Univ.Instance.hcons u) -let hcons_pcon (c,u) = (hcons_con c, Univ.Instance.hcons u) +let hcons_pconstruct (c,u as x) = + let c' = hcons_construct c in + if c' == c then x + else (c', u) + +let hcons_pind (i,u as x) = + let i' = hcons_ind i in + if i' == i then x + else i', u + +let hcons_pcon (c,u as x) = + let c' = hcons_con c in + if c' == c then x + else c', u + +(* let hcons_pconstruct (c,u) = (hcons_construct c, Univ.Instance.hcons u) *) +(* let hcons_pind (i,u) = (hcons_ind i, Univ.Instance.hcons u) *) +(* let hcons_pcon (c,u) = (hcons_con c, Univ.Instance.hcons u) *) let hcons = hashcons diff --git a/kernel/univ.ml b/kernel/univ.ml index 88b4e650f..2b512d76f 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1679,22 +1679,23 @@ struct let hash = HInstancestruct.hash - let share a = - let len = Array.length a in - if Int.equal len 0 then (empty, 0) - else begin - let accu = ref 0 in - for i = 0 to len - 1 do - let l = Array.unsafe_get a i in - let l', h = Level.hcons l, Level.hash l in - accu := Hashset.Combine.combine !accu h; - if l' == l then () - else Array.unsafe_set a i l' - done; - (* [h] must be positive. *) - let h = !accu land 0x3FFFFFFF in - (a, h) - end + let share a = (a, hash a) + + (* let len = Array.length a in *) + (* if Int.equal len 0 then (empty, 0) *) + (* else begin *) + (* let accu = ref 0 in *) + (* for i = 0 to len - 1 do *) + (* let l = Array.unsafe_get a i in *) + (* let l', h = Level.hcons l, Level.hash l in *) + (* accu := Hashset.Combine.combine !accu h; *) + (* if l' == l then () *) + (* else Array.unsafe_set a i l' *) + (* done; *) + (* (\* [h] must be positive. *\) *) + (* let h = !accu land 0x3FFFFFFF in *) + (* (a, h) *) + (* end *) let empty = hcons [||] diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index c11a26fb2..f2da99c13 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -276,12 +276,16 @@ let close_proof ?feedback_id ~now fpl = let compute_univs (usubst, uctx) = let nf = Universes.nf_evars_and_universes_opt_subst (fun _ -> None) usubst in let compute_c_t (c, eff) = - let univs = - Univ.LSet.union (Universes.universes_of_constr c) - (Universes.universes_of_constr t) - in - let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context uctx) univs in - (nf c, eff), nf t, Univ.ContextSet.to_context ctx + let c, t = + if not now then nf c, nf t + else (* Already normalized below *) c, nf t + in + let univs = + Univ.LSet.union (Universes.universes_of_constr c) + (Universes.universes_of_constr t) + in + let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context uctx) univs in + (c, eff), t, Univ.ContextSet.to_context ctx in Future.chain ~pure:true p compute_c_t in @@ -309,7 +313,7 @@ let close_proof ?feedback_id ~now fpl = else Univ.ContextSet.empty in let _ = - if now then + if poly || now then List.iter (fun x -> ignore(Future.compute x.Entries.const_entry_body)) entries in (* let hook = Option.map (fun f -> @@ -345,7 +349,7 @@ let return_proof () = (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) - let proofs = List.map (fun (c, _) -> (Evarutil.nf_evar evd c, eff)) initial_goals in + let proofs = List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd c, eff)) initial_goals in proofs, (subst, ctx) let close_future_proof ~feedback_id proof = |