diff options
Diffstat (limited to 'plugins/ssr/ssrparser.ml4')
| -rw-r--r-- | plugins/ssr/ssrparser.ml4 | 24 |
1 files changed, 11 insertions, 13 deletions
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 09917339a7..060225dab7 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -8,8 +8,6 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) -open API -open Grammar_API open Names open Pp open Pcoq @@ -64,7 +62,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,Ppextend.E) +let tacltop = (5,Notation_term.E) let pr_ssrtacarg _ _ prt = prt tacltop ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY pr_ssrtacarg @@ -344,7 +342,7 @@ let interp_index ist gl idx = | None -> begin match Tacinterp.Value.to_constr v with | Some c -> - let rc = Detyping.detype false [] (pf_env gl) (project gl) c in + let rc = Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) c in begin match Notation.uninterp_prim_token rc with | _, Constrexpr.Numeral (s,b) -> let n = int_of_string s in if b then n else -n @@ -1064,32 +1062,32 @@ let rec format_glob_decl h0 d0 = match h0, d0 with Bdef (x, None, v) :: format_glob_decl [] d | _, [] -> [] -let rec format_glob_constr h0 c0 = let open CAst in match h0, c0 with - | BFvar :: h, { v = GLambda (x, _, _, c) } -> +let rec format_glob_constr h0 c0 = match h0, DAst.get c0 with + | BFvar :: h, GLambda (x, _, _, c) -> let bs, c' = format_glob_constr h c in Bvar x :: bs, c' - | BFdecl 1 :: h, { v = GLambda (x, _, t, c) } -> + | BFdecl 1 :: h, GLambda (x, _, t, c) -> let bs, c' = format_glob_constr h c in Bdecl ([x], t) :: bs, c' - | BFdecl n :: h, { v = GLambda (x, _, t, c) } when n > 1 -> + | BFdecl n :: h, GLambda (x, _, t, c) when n > 1 -> begin match format_glob_constr (BFdecl (n - 1) :: h) c with | Bdecl (xs, _) :: bs, c' -> Bdecl (x :: xs, t) :: bs, c' | _ -> [Bdecl ([x], t)], c end - | BFdef :: h, { v = GLetIn(x, v, oty, c) } -> + | BFdef :: h, GLetIn(x, v, oty, c) -> let bs, c' = format_glob_constr h c in Bdef (x, oty, v) :: bs, c' - | [BFcast], { v = GCast (c, CastConv t) } -> + | [BFcast], GCast (c, CastConv t) -> [Bcast t], c - | BFrec (has_str, has_cast) :: h, { v = GRec (f, _, bl, t, c) } + | BFrec (has_str, has_cast) :: h, GRec (f, _, bl, t, c) when Array.length c = 1 -> let bs = format_glob_decl h bl.(0) in let bstr = match has_str, f with | true, GFix ([|Some i, GStructRec|], _) -> mkBstruct i bs | _ -> [] in bs @ bstr @ (if has_cast then [Bcast t.(0)] else []), c.(0) - | _, c -> - [], c + | _, _ -> + [], c0 (** Forward chaining argument *) |