diff options
Diffstat (limited to 'plugins/ssr/ssrparser.ml4')
-rw-r--r-- | plugins/ssr/ssrparser.ml4 | 53 |
1 files changed, 21 insertions, 32 deletions
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 0d82a9f09..352f88bb3 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -10,6 +10,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +let _vmcast = Constr.VMcast open Names open Pp open Pcoq @@ -17,18 +18,19 @@ open Ltac_plugin open Genarg open Stdarg open Tacarg -open Term open Libnames open Tactics open Tacmach open Util +open Locus open Tacexpr open Tacinterp open Pltac open Extraargs open Ppconstr -open Misctypes +open Namegen +open Tactypes open Decl_kinds open Constrexpr open Constrexpr_ops @@ -64,7 +66,7 @@ DECLARE PLUGIN "ssreflect_plugin" * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = CLexer.get_keyword_state () ;; -let tacltop = (5,Notation_term.E) +let tacltop = (5,Notation_gram.E) let pr_ssrtacarg _ _ prt = prt tacltop ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY pr_ssrtacarg @@ -301,24 +303,24 @@ END let pr_index = function - | Misctypes.ArgVar {CAst.v=id} -> pr_id id - | Misctypes.ArgArg n when n > 0 -> int n + | ArgVar {CAst.v=id} -> pr_id id + | ArgArg n when n > 0 -> int n | _ -> mt () let pr_ssrindex _ _ _ = pr_index -let noindex = Misctypes.ArgArg 0 +let noindex = ArgArg 0 let check_index ?loc i = if i > 0 then i else CErrors.user_err ?loc (str"Index not positive") let mk_index ?loc = function - | Misctypes.ArgArg i -> Misctypes.ArgArg (check_index ?loc i) + | ArgArg i -> ArgArg (check_index ?loc i) | iv -> iv let interp_index ist gl idx = Tacmach.project gl, match idx with - | Misctypes.ArgArg _ -> idx - | Misctypes.ArgVar id -> + | ArgArg _ -> idx + | ArgVar id -> let i = try let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in @@ -336,7 +338,7 @@ let interp_index ist gl idx = | None -> raise Not_found end end with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in - Misctypes.ArgArg (check_index ?loc:id.CAst.loc i) + ArgArg (check_index ?loc:id.CAst.loc i) open Pltac @@ -543,7 +545,7 @@ END let remove_loc x = x.CAst.v -let ipat_of_intro_pattern p = Misctypes.( +let ipat_of_intro_pattern p = Tactypes.( let rec ipat_of_intro_pattern = function | IntroNaming (IntroIdentifier id) -> IPatId id | IntroAction IntroWildcard -> IPatAnon Drop @@ -585,37 +587,25 @@ let pr_ssripat _ _ _ = pr_ipat let pr_ssripats _ _ _ = pr_ipats let pr_ssriorpat _ _ _ = pr_iorpat -(* -let intern_ipat ist ipat = - let rec check_pat = function - | IPatClear clr -> ignore (List.map (intern_hyp ist) clr) - | IPatCase iorpat -> List.iter (List.iter check_pat) iorpat - | IPatDispatch iorpat -> List.iter (List.iter check_pat) iorpat - | IPatInj iorpat -> List.iter (List.iter check_pat) iorpat - | _ -> () in - check_pat ipat; ipat -*) - let intern_ipat ist = map_ipat (fun id -> id) - (intern_hyp ist) (* TODO: check with ltac, old code was ignoring the result *) + (intern_hyp ist) (glob_ast_closure_term ist) let intern_ipats ist = List.map (intern_ipat ist) let interp_intro_pattern = interp_wit wit_intro_pattern -let interp_introid ist gl id = Misctypes.( +let interp_introid ist gl id = try IntroNaming (IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (Loc.tag id)))))) with _ -> (snd (interp_intro_pattern ist gl (CAst.make @@ IntroNaming (IntroIdentifier id)))).CAst.v -) let get_intro_id = function | IntroNaming (IntroIdentifier id) -> id | _ -> assert false -let rec add_intro_pattern_hyps ipat hyps = Misctypes.( +let rec add_intro_pattern_hyps ipat hyps = let {CAst.loc=loc;v=ipat} = ipat in match ipat with | IntroNaming (IntroIdentifier id) -> @@ -634,7 +624,6 @@ let rec add_intro_pattern_hyps ipat hyps = Misctypes.( | IntroForthcoming _ -> (* As in ipat_of_intro_pattern, was unable to determine which kind of ipat interp_introid could return [HH] *) assert false -) (* We interp the ipat using the standard ltac machinery for ids, since * we have no clue what a name could be bound to (maybe another ipat) *) @@ -1075,7 +1064,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } -> let bs, c' = format_constr_expr h c in Bdef (x, oty, v) :: bs, c' - | [BFcast], { v = CCast (c, CastConv t) } -> + | [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]) } -> @@ -1104,7 +1093,7 @@ let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt let mkFwdVal fk c = ((fk, []), c) let mkssrFwdVal fk c = ((fk, []), (c,None)) -let dC t = CastConv t +let dC t = Glob_term.CastConv t let same_ist { interp_env = x } { interp_env = y } = match x,y with @@ -1221,8 +1210,8 @@ let push_binders c2 bs = | [] -> c | _ -> anomaly "binder not a lambda nor a let in" in match c2 with - | { loc; v = CCast (ct, CastConv cty) } -> - CAst.make ?loc @@ (CCast (loop false ct bs, CastConv (loop true cty bs))) + | { loc; v = CCast (ct, Glob_term.CastConv cty) } -> + CAst.make ?loc @@ (CCast (loop false ct bs, Glob_term.CastConv (loop true cty bs))) | ct -> loop false ct bs let rec fix_binders = let open CAst in function @@ -1949,7 +1938,7 @@ END let vmexacttac pf = Goal.nf_enter begin fun gl -> - exact_no_check (EConstr.mkCast (pf, VMcast, Tacmach.New.pf_concl gl)) + exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl)) end TACTIC EXTEND ssrexact |