diff options
| -rw-r--r-- | src/tac2core.ml | 3 | ||||
| -rw-r--r-- | src/tac2print.ml | 15 | ||||
| -rw-r--r-- | src/tac2stdlib.ml | 6 | ||||
| -rw-r--r-- | src/tac2tactics.ml | 18 | ||||
| -rw-r--r-- | src/tac2tactics.mli | 2 |
5 files changed, 29 insertions, 15 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index fe4912a6c5..32c873088c 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -895,7 +895,8 @@ let () = let intern self ist c = let env = ist.Genintern.genv in let sigma = Evd.from_env env in - let _, pat = Constrintern.intern_constr_pattern env sigma ~as_type:false c in + let warn = if !Ltac_plugin.Tacintern.strict_check then fun x -> x else Constrintern.for_grammar in + let _, pat = warn (fun () ->Constrintern.intern_constr_pattern env sigma ~as_type:false c) () in GlbVal pat, gtypref t_pattern in let print env pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env Evd.empty pat ++ str ")" in diff --git a/src/tac2print.ml b/src/tac2print.ml index 8f61686988..cab1530d15 100644 --- a/src/tac2print.ml +++ b/src/tac2print.ml @@ -390,7 +390,9 @@ let rec pr_valexpr env sigma v t = match kind t with let knc = change_kn_label kn id in let args = pr_constrargs env sigma params args tpe in hv 2 (pr_constructor knc ++ spc () ++ str "(" ++ args ++ str ")") - | GTydRec rcd -> str "{ TODO }" + | GTydRec rcd -> + let (_, args) = Tac2ffi.to_block v in + pr_record env sigma params args rcd | GTydOpn -> begin match Tac2ffi.to_open v with | (knc, [||]) -> pr_constructor knc @@ -417,6 +419,17 @@ and pr_constrargs env sigma params args tpe = let args = List.combine args tpe in prlist_with_sep pr_comma (fun (v, t) -> pr_valexpr env sigma v t) args +and pr_record env sigma params args rcd = + let subst = Array.of_list params in + let map (id, _, tpe) = (id, subst_type subst tpe) in + let rcd = List.map map rcd in + let args = Array.to_list args in + let fields = List.combine rcd args in + let pr_field ((id, t), arg) = + Id.print id ++ spc () ++ str ":=" ++ spc () ++ pr_valexpr env sigma arg t + in + str "{" ++ spc () ++ prlist_with_sep pr_semicolon pr_field fields ++ spc () ++ str "}" + and pr_val_list env sigma args tpe = let pr v = pr_valexpr env sigma v tpe in str "[" ++ prlist_with_sep pr_semicolon pr args ++ str "]" diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml index 28d4967874..9ed3d5b32e 100644 --- a/src/tac2stdlib.ml +++ b/src/tac2stdlib.ml @@ -186,9 +186,9 @@ let to_strategy v = match Value.to_int v with let strategy = make_to_repr to_strategy let to_inversion_kind v = match Value.to_int v with -| 0 -> Misctypes.SimpleInversion -| 1 -> Misctypes.FullInversion -| 2 -> Misctypes.FullInversionClear +| 0 -> Inv.SimpleInversion +| 1 -> Inv.FullInversion +| 2 -> Inv.FullInversionClear | _ -> assert false let inversion_kind = make_to_repr to_inversion_kind diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml index 9bc23e91d7..3f2385a8d6 100644 --- a/src/tac2tactics.ml +++ b/src/tac2tactics.ml @@ -106,9 +106,9 @@ let apply adv ev cb cl = let mk_destruction_arg = function | ElimOnConstr c -> let c = c >>= fun c -> return (mk_with_bindings c) in - Misctypes.ElimOnConstr (delayed_of_tactic c) -| ElimOnIdent id -> Misctypes.ElimOnIdent CAst.(make id) -| ElimOnAnonHyp n -> Misctypes.ElimOnAnonHyp n + Tactics.ElimOnConstr (delayed_of_tactic c) +| ElimOnIdent id -> Tactics.ElimOnIdent CAst.(make id) +| ElimOnAnonHyp n -> Tactics.ElimOnAnonHyp n let mk_induction_clause (arg, eqn, as_, occ) = let eqn = Option.map (fun ipat -> CAst.make @@ mk_intro_pattern_naming ipat) eqn in @@ -342,9 +342,9 @@ let on_destruction_arg tac ev arg = Proofview.tclEVARMAP >>= fun sigma' -> let flags = tactic_infer_flags ev in let (sigma', c) = Unification.finish_evar_resolution ~flags env sigma' (sigma, c) in - Proofview.tclUNIT (Some sigma', Misctypes.ElimOnConstr (c, lbind)) - | ElimOnIdent id -> Proofview.tclUNIT (None, Misctypes.ElimOnIdent CAst.(make id)) - | ElimOnAnonHyp n -> Proofview.tclUNIT (None, Misctypes.ElimOnAnonHyp n) + Proofview.tclUNIT (Some sigma', Tactics.ElimOnConstr (c, lbind)) + | ElimOnIdent id -> Proofview.tclUNIT (None, Tactics.ElimOnIdent CAst.(make id)) + | ElimOnAnonHyp n -> Proofview.tclUNIT (None, Tactics.ElimOnAnonHyp n) in arg >>= fun (sigma', arg) -> let arg = Some (clear, arg) in @@ -427,11 +427,11 @@ let inversion knd arg pat ids = let inversion _ arg = begin match arg with | None -> assert false - | Some (_, Misctypes.ElimOnAnonHyp n) -> + | Some (_, Tactics.ElimOnAnonHyp n) -> Inv.inv_clause knd pat ids (AnonHyp n) - | Some (_, Misctypes.ElimOnIdent {CAst.v=id}) -> + | Some (_, Tactics.ElimOnIdent {CAst.v=id}) -> Inv.inv_clause knd pat ids (NamedHyp id) - | Some (_, Misctypes.ElimOnConstr c) -> + | Some (_, Tactics.ElimOnConstr c) -> let open Misctypes in let anon = CAst.make @@ IntroNaming IntroAnonymous in Tactics.specialize c (Some anon) >>= fun () -> diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli index 52e8a94c19..631e36b5ae 100644 --- a/src/tac2tactics.mli +++ b/src/tac2tactics.mli @@ -118,7 +118,7 @@ val eauto : Hints.debug -> int option -> int option -> constr thunk list -> val typeclasses_eauto : Class_tactics.search_strategy option -> int option -> Id.t list option -> unit Proofview.tactic -val inversion : Misctypes.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic +val inversion : Inv.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic val contradiction : constr_with_bindings option -> unit tactic |