diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/extraction.ml | 8 | ||||
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 2 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 12 |
3 files changed, 10 insertions, 12 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 3a61c7747..71e09992c 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -488,7 +488,7 @@ and extract_really_ind env kn mib = Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l)) then raise (I Singleton); if List.is_empty l then raise (I Standard); - if Option.is_empty mib.mind_record then raise (I Standard); + if mib.mind_record == Declarations.NotRecord then raise (I Standard); (* Now we're sure it's a record. *) (* First, we find its field names. *) let rec names_prod t = match Constr.kind t with @@ -1069,8 +1069,7 @@ let extract_constant env kn cb = | false -> mk_typ (get_body c) | true -> let pb = lookup_projection (Projection.make kn false) env in - (** FIXME: handle mutual records *) - let ind = (pb.Declarations.proj_ind, 0) in + let ind = pb.Declarations.proj_ind in let bodies = Inductiveops.legacy_match_projection env ind in let body = bodies.(pb.Declarations.proj_arg) in mk_typ (EConstr.of_constr body)) @@ -1086,8 +1085,7 @@ let extract_constant env kn cb = | false -> mk_def (get_body c) | true -> let pb = lookup_projection (Projection.make kn false) env in - (** FIXME: handle mutual records *) - let ind = (pb.Declarations.proj_ind, 0) in + let ind = pb.Declarations.proj_ind in let bodies = Inductiveops.legacy_match_projection env ind in let body = bodies.(pb.Declarations.proj_arg) in mk_def (EConstr.of_constr body)) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 2c046190f..7fe2421f9 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -47,6 +47,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = let cl = EConstr.Unsafe.to_constr cl in try fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1 with NoMatch -> redex_of_pattern ~resolve_typeclasses:true env pat, cl in + let gl = pf_merge_uc ucst gl in let c = EConstr.of_constr c in let cl = EConstr.of_constr cl in if Termops.occur_existential sigma c then errorstrm(str"The pattern"++spc()++ @@ -56,7 +57,6 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = | Cast(t, DEFAULTcast, ty) -> t, (gl, ty) | _ -> c, pfe_type_of gl c in let cl' = EConstr.mkLetIn (Name id, c, cty, cl) in - let gl = pf_merge_uc ucst gl in Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl cl')) (introid id) gl open Util diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index c20e415b4..9d9b1b2e8 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -561,8 +561,8 @@ let filter_upat i0 f n u fpats = let na = Array.length u.up_a in if n < na then fpats else let np = match u.up_k with - | KpatConst when equal u.up_f f -> na - | KpatFixed when equal u.up_f f -> na + | KpatConst when eq_constr_nounivs u.up_f f -> na + | KpatFixed when eq_constr_nounivs u.up_f f -> na | KpatEvar k when isEvar_k k f -> na | KpatLet when isLetIn f -> na | KpatLam when isLambda f -> na @@ -582,8 +582,8 @@ let filter_upat_FO i0 f n u fpats = let np = nb_args u.up_FO in if n < np then fpats else let ok = match u.up_k with - | KpatConst -> equal u.up_f f - | KpatFixed -> equal u.up_f f + | KpatConst -> eq_constr_nounivs u.up_f f + | KpatFixed -> eq_constr_nounivs u.up_f f | KpatEvar k -> isEvar_k k f | KpatLet -> isLetIn f | KpatLam -> isLambda f @@ -764,8 +764,8 @@ let mk_tpattern_matcher ?(all_instances=false) let match_let f = match kind f with | LetIn (_, v, _, b) -> unif_EQ env sigma pv v && unif_EQ env' sigma pb b | _ -> false in match_let - | KpatFixed -> equal u.up_f - | KpatConst -> equal u.up_f + | KpatFixed -> eq_constr_nounivs u.up_f + | KpatConst -> eq_constr_nounivs u.up_f | KpatLam -> fun c -> (match kind c with | Lambda _ -> unif_EQ env sigma u.up_f c |