diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 6 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mlg | 4 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.mlg | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrview.ml | 2 |
5 files changed, 8 insertions, 8 deletions
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 350bb9019e..675e4d2457 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -194,7 +194,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let sort = Tacticals.elimination_sort_of_goal gl in let gl, elim = if not is_case then - let t,gl= pf_fresh_global (Indrec.lookup_eliminator (kn,i) sort) gl in + let t,gl= pf_fresh_global (Indrec.lookup_eliminator env (kn,i) sort) gl in gl, t else Tacmach.pf_eapply (fun env sigma () -> diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 5abbc214de..4433f2fce7 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -340,7 +340,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let elim, gl = let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in let sort = elimination_sort_of_goal gl in - let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in + let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in if dir = R2L then elim, gl else (* taken from Coq's rewrite *) let elim, _ = destConst elim in let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in @@ -504,9 +504,9 @@ let rwprocess_rule dir rule gl = let sigma, rs2 = loop d sigma s a.(1) rs 0 in let s, sigma = sr sigma 1 in loop d sigma s a.(0) rs2 0 - | App (r_eq, a) when Hipattern.match_with_equality_type sigma t != None -> + | App (r_eq, a) when Hipattern.match_with_equality_type env sigma t != None -> let (ind, u) = EConstr.destInd sigma r_eq and rhs = Array.last a in - let np = Inductiveops.inductive_nparamdecls ind in + let np = Inductiveops.inductive_nparamdecls env ind in let indu = (ind, EConstr.EInstance.kind sigma u) in let ind_ct = Inductiveops.type_of_constructors env indu in let lhs0 = last_arg sigma (EConstr.of_constr (strip_prod_assum ind_ct.(0))) in diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 7cd62f4ead..f44962f213 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -1200,7 +1200,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with | [BFcast], { v = CCast (c, Glob_term.CastConv t) } -> [Bcast t], c | BFrec (has_str, has_cast) :: h, - { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } -> + { v = CFix ( _, [_, Some {CAst.v = CStructRec locn}, bl, t, c]) } -> let bs = format_local_binders h bl in let bstr = if has_str then [Bstruct (Name locn.CAst.v)] else [] in bs @ bstr @ (if has_cast then [Bcast t] else []), c @@ -1424,7 +1424,7 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS (ident * ssrfwd) PRINTED BY { pr_ssrfixfwd } | [] -> CErrors.user_err (Pp.str "Bad structural argument") in loop (names_of_local_assums lb) in let h' = BFrec (has_struct, has_cast) :: binders_fmts bs in - let fix = CAst.make ~loc @@ CFix (lid, [lid, (Some i, CStructRec), lb, t', c']) in + let fix = CAst.make ~loc @@ CFix (lid, [lid, (Some (CAst.make (CStructRec i))), lb, t', c']) in id, ((fk, h'), { ac with body = fix }) } END diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 0a0d9b12fa..bf7f082192 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -183,7 +183,7 @@ GRAMMAR EXTEND Gram GLOBAL: gallina_ext; gallina_ext: [ [ IDENT "Import"; IDENT "Prenex"; IDENT "Implicits" -> - { Vernacexpr.VernacUnsetOption (false, ["Printing"; "Implicit"; "Defensive"]) } + { Vernacexpr.VernacSetOption (false, ["Printing"; "Implicit"; "Defensive"], Vernacexpr.OptionUnset) } ] ] ; END diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 537fd7d7b4..075ebf006a 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -43,7 +43,7 @@ module AdaptorDb = struct term_view_adaptor_db := AdaptorMap.add k (t :: lk) !term_view_adaptor_db let subst_adaptor ( subst, (k, t as a)) = - let t' = Detyping.subst_glob_constr subst t in + let t' = Detyping.subst_glob_constr (Global.env()) subst t in if t' == t then a else k, t' let in_db = |