diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/Ltac.v | 0 | ||||
| -rw-r--r-- | plugins/ltac/extraargs.mlg | 2 | ||||
| -rw-r--r-- | plugins/ltac/extraargs.mli | 2 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.ml | 103 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.mli | 29 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.ml | 6 | ||||
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 30 | ||||
| -rw-r--r-- | plugins/ltac/tactic_matching.ml | 19 |
8 files changed, 101 insertions, 90 deletions
diff --git a/plugins/ltac/Ltac.v b/plugins/ltac/Ltac.v deleted file mode 100644 index e69de29bb2..0000000000 --- a/plugins/ltac/Ltac.v +++ /dev/null diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index bab6bfd78e..5835d75c79 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -298,7 +298,7 @@ END let pr_by_arg_tac env sigma _prc _prlc prtac opt_c = match opt_c with | None -> mt () - | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (3,Notation_gram.E) t) + | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (Constrexpr.LevelLe 3) t) } diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 6dd51e4e01..dd4195f2ef 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -67,7 +67,7 @@ val wit_by_arg_tac : val pr_by_arg_tac : Environ.env -> Evd.evar_map -> - (Environ.env -> Evd.evar_map -> int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> raw_tactic_expr -> Pp.t) -> raw_tactic_expr option -> Pp.t val test_lpar_id_colon : unit Pcoq.Entry.t diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 7843faaef3..e2b8bcb5a9 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -17,7 +17,6 @@ open Constrexpr open Genarg open Geninterp open Stdarg -open Notation_gram open Tactypes open Locus open Genredexpr @@ -73,43 +72,43 @@ type 'a raw_extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) -> 'a -> Pp.t type 'a glob_extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) -> 'a -> Pp.t type 'a extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) -> 'a -> Pp.t type 'a raw_extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t type 'a glob_extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t type 'a extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t let string_of_genarg_arg (ArgumentType arg) = let rec aux : type a b c. (a, b, c) genarg_type -> string = function @@ -294,7 +293,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr _ = str "_" in KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)" - let pr_farg prtac arg = prtac (1, Any) (TacArg (CAst.make arg)) + let pr_farg prtac arg = prtac LevelSome (TacArg (CAst.make arg)) let is_genarg tag wit = let ArgT.Any tag = tag in @@ -314,35 +313,35 @@ let string_of_genarg_arg (ArgumentType arg) = let rec pr_any_arg : type l. (_ -> l generic_argument -> Pp.t) -> _ -> l generic_argument -> Pp.t = fun prtac symb arg -> match symb with - | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg + | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac LevelSome arg | Extend.Ulist1 s | Extend.Ulist0 s -> begin match get_list arg with - | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" | Some l -> pr_sequence (pr_any_arg prtac s) l end | Extend.Ulist1sep (s, sep) | Extend.Ulist0sep (s, sep) -> begin match get_list arg with - | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" | Some l -> prlist_with_sep (fun () -> str sep) (pr_any_arg prtac s) l end | Extend.Uopt s -> begin match get_opt arg with - | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" | Some l -> pr_opt (pr_any_arg prtac s) l end | Extend.Uentry _ | Extend.Uentryl _ -> - str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + str "ltac:(" ++ prtac LevelSome arg ++ str ")" let pr_targ prtac symb arg = match symb with | Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) -> - prtac (1, Any) arg - | Extend.Uentryl (_, l) -> prtac (l, Any) arg + prtac LevelSome arg + | Extend.Uentryl (_, l) -> prtac LevelSome arg | _ -> match arg with | TacGeneric arg -> let pr l arg = prtac l (TacGeneric arg) in pr_any_arg pr symb arg - | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" + | _ -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" let pr_raw_extend_rec prtac = pr_extend_gen (pr_farg prtac) @@ -630,7 +629,7 @@ let pr_goal_selector ~toplevel s = let pr_then () = str ";" - let ltop = (5,E) + let ltop = LevelLe 5 let lseq = 4 let ltactical = 3 let lorelse = 2 @@ -645,13 +644,13 @@ let pr_goal_selector ~toplevel s = let ltatom = 1 let linfo = 5 - let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq + let level_of p = match p with LevelLe n -> n | LevelLt n -> n-1 | LevelSome -> lseq (** A printer for tactics that polymorphically works on the three "raw", "glob" and "typed" levels *) type 'a printer = { - pr_tactic : tolerability -> 'tacexpr -> Pp.t; + pr_tactic : entry_relative_level -> 'tacexpr -> Pp.t; pr_constr : Environ.env -> Evd.evar_map -> 'trm -> Pp.t; pr_lconstr : Environ.env -> Evd.evar_map -> 'trm -> Pp.t; pr_dconstr : Environ.env -> Evd.evar_map -> 'dtrm -> Pp.t; @@ -780,7 +779,7 @@ let pr_goal_selector ~toplevel s = hov 1 ( primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++ pr_assumption (pr.pr_constr env sigma) (pr.pr_dconstr env sigma) (pr.pr_lconstr env sigma) ipat c ++ - pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac + pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (LevelLe ltactical))) tac ) | TacAssert (ev,_,None,ipat,c) -> hov 1 ( @@ -857,7 +856,7 @@ let pr_goal_selector ~toplevel s = pr_with_bindings_arg_full (pr.pr_dconstr env sigma) (pr.pr_dconstr env sigma) c) l ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl - ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac + ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (LevelLe ltactical))) tac ) | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 ( @@ -893,11 +892,11 @@ let pr_goal_selector ~toplevel s = let return (doc, l) = (tag tac doc, l) in let (strm, prec) = return (match tac with | TacAbstract (t,None) -> - keyword "abstract " ++ pr_tac (labstract,L) t, labstract + keyword "abstract " ++ pr_tac (LevelLt labstract) t, labstract | TacAbstract (t,Some s) -> hov 0 ( keyword "abstract" - ++ str" (" ++ pr_tac (labstract,L) t ++ str")" ++ spc () + ++ str" (" ++ pr_tac (LevelLt labstract) t ++ str")" ++ spc () ++ keyword "using" ++ spc () ++ pr_id s), labstract | TacLetIn (recflag,llc,u) -> @@ -906,7 +905,7 @@ let pr_goal_selector ~toplevel s = (hv 0 ( pr_let_clauses recflag (pr.pr_generic env sigma) (pr_tac ltop) llc ++ spc () ++ keyword "in" - ) ++ fnl () ++ pr_tac (llet,E) u), + ) ++ fnl () ++ pr_tac (LevelLe llet) u), llet | TacMatch (lz,t,lrul) -> hov 0 ( @@ -931,17 +930,17 @@ let pr_goal_selector ~toplevel s = hov 2 ( keyword "fun" ++ prlist pr_funvar lvar ++ str " =>" ++ spc () - ++ pr_tac (lfun,E) body), + ++ pr_tac (LevelLe lfun) body), lfun | TacThens (t,tl) -> hov 1 ( - pr_tac (lseq,E) t ++ pr_then () ++ spc () + pr_tac (LevelLe lseq) t ++ pr_then () ++ spc () ++ pr_seq_body (pr_opt_tactic (pr_tac ltop)) tl), lseq | TacThen (t1,t2) -> hov 1 ( - pr_tac (lseq,E) t1 ++ pr_then () ++ spc () - ++ pr_tac (lseq,L) t2), + pr_tac (LevelLe lseq) t1 ++ pr_then () ++ spc () + ++ pr_tac (LevelLt lseq) t2), lseq | TacDispatch tl -> pr_dispatch (pr_tac ltop) tl, lseq @@ -949,78 +948,78 @@ let pr_goal_selector ~toplevel s = pr_tac_extend (pr_tac ltop) tf t tr , lseq | TacThens3parts (t1,tf,t2,tl) -> hov 1 ( - pr_tac (lseq,E) t1 ++ pr_then () ++ spc () + pr_tac (LevelLe lseq) t1 ++ pr_then () ++ spc () ++ pr_then_gen (pr_tac ltop) tf t2 tl), lseq | TacTry t -> hov 1 ( - keyword "try" ++ spc () ++ pr_tac (ltactical,E) t), + keyword "try" ++ spc () ++ pr_tac (LevelLe ltactical) t), ltactical | TacDo (n,t) -> hov 1 ( str "do" ++ spc () ++ pr_or_var int n ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacTimeout (n,t) -> hov 1 ( keyword "timeout " ++ pr_or_var int n ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacTime (s,t) -> hov 1 ( keyword "time" ++ pr_opt qstring s ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacRepeat t -> hov 1 ( keyword "repeat" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacProgress t -> hov 1 ( keyword "progress" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacShowHyps t -> hov 1 ( keyword "infoH" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacInfo t -> hov 1 ( keyword "info" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), linfo | TacOr (t1,t2) -> hov 1 ( - pr_tac (lorelse,L) t1 ++ spc () + pr_tac (LevelLt lorelse) t1 ++ spc () ++ str "+" ++ brk (1,1) - ++ pr_tac (lorelse,E) t2), + ++ pr_tac (LevelLe lorelse) t2), lorelse | TacOnce t -> hov 1 ( keyword "once" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacExactlyOnce t -> hov 1 ( keyword "exactly_once" ++ spc () - ++ pr_tac (ltactical,E) t), + ++ pr_tac (LevelLe ltactical) t), ltactical | TacIfThenCatch (t,tt,te) -> hov 1 ( - str"tryif" ++ spc() ++ pr_tac (ltactical,E) t ++ brk(1,1) ++ - str"then" ++ spc() ++ pr_tac (ltactical,E) tt ++ brk(1,1) ++ - str"else" ++ spc() ++ pr_tac (ltactical,E) te ++ brk(1,1)), + str"tryif" ++ spc() ++ pr_tac (LevelLe ltactical) t ++ brk(1,1) ++ + str"then" ++ spc() ++ pr_tac (LevelLe ltactical) tt ++ brk(1,1) ++ + str"else" ++ spc() ++ pr_tac (LevelLe ltactical) te ++ brk(1,1)), ltactical | TacOrelse (t1,t2) -> hov 1 ( - pr_tac (lorelse,L) t1 ++ spc () + pr_tac (LevelLt lorelse) t1 ++ spc () ++ str "||" ++ brk (1,1) - ++ pr_tac (lorelse,E) t2), + ++ pr_tac (LevelLe lorelse) t2), lorelse | TacFail (g,n,l) -> let arg = @@ -1042,7 +1041,7 @@ let pr_goal_selector ~toplevel s = | TacSolve tl -> keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet | TacComplete t -> - pr_tac (lcomplete,E) t, lcomplete + pr_tac (LevelLe lcomplete) t, lcomplete | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom | TacId l -> keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom @@ -1398,10 +1397,10 @@ let () = let () = let printer env sigma _ _ prtac = prtac env sigma in declare_extra_genarg_pprule_with_level wit_tactic printer printer printer - ltop (0,E) + ltop (LevelLe 0) let () = let pr_unit _env _sigma _ _ _ _ () = str "()" in let printer env sigma _ _ prtac = prtac env sigma in declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit - ltop (0,E) + ltop (LevelLe 0) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 9cff3ea1eb..33db933168 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -16,7 +16,6 @@ open Geninterp open Names open Environ open Constrexpr -open Notation_gram open Genintern open Tacexpr open Tactypes @@ -29,43 +28,43 @@ type 'a raw_extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) -> 'a -> Pp.t type 'a glob_extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) -> 'a -> Pp.t type 'a extra_genarg_printer = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> + (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) -> 'a -> Pp.t type 'a raw_extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t type 'a glob_extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t type 'a extra_genarg_printer_with_level = Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) -> - (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) -> - tolerability -> 'a -> Pp.t + (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) -> + entry_relative_level -> 'a -> Pp.t val declare_extra_genarg_pprule : ('a, 'b, 'c) genarg_type -> @@ -78,7 +77,7 @@ val declare_extra_genarg_pprule_with_level : 'a raw_extra_genarg_printer_with_level -> 'b glob_extra_genarg_printer_with_level -> 'c extra_genarg_printer_with_level -> - (* surroounded *) tolerability -> (* non-surroounded *) tolerability -> unit + (* surroounded *) entry_relative_level -> (* non-surroounded *) entry_relative_level -> unit val declare_extra_vernac_genarg_pprule : ('a, 'b, 'c) genarg_type -> @@ -140,7 +139,7 @@ val pr_ltac_constant : ltac_constant -> Pp.t val pr_raw_tactic : env -> Evd.evar_map -> raw_tactic_expr -> Pp.t -val pr_raw_tactic_level : env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t +val pr_raw_tactic_level : env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t val pr_glob_tactic : env -> glob_tactic_expr -> Pp.t @@ -155,10 +154,10 @@ val pr_match_pattern : ('a -> Pp.t) -> 'a match_pattern -> Pp.t val pr_match_rule : bool -> ('a -> Pp.t) -> ('b -> Pp.t) -> ('b, 'a) match_rule -> Pp.t -val pr_value : tolerability -> Val.t -> Pp.t +val pr_value : entry_relative_level -> Val.t -> Pp.t -val ltop : tolerability +val ltop : entry_relative_level -val make_constr_printer : (env -> Evd.evar_map -> tolerability -> 'a -> Pp.t) -> +val make_constr_printer : (env -> Evd.evar_map -> entry_relative_level -> 'a -> Pp.t) -> 'a Genprint.top_printer diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 13a2f3b8c0..8b4520947b 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) state = in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in - let r = ExtendRule (entry, None, (pos, [(None, None, [rules])])) in + let r = ExtendRule (entry, (pos, [(None, None, [rules])])) in ([r], state) let tactic_grammar = @@ -415,7 +415,7 @@ let create_ltac_quotation name cast (e, l) = in let action _ v _ _ _ loc = cast (Some loc, v) in let gram = (level, assoc, [Rule (rule, action)]) in - Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram]) + Pcoq.grammar_extend Pltac.tactic_arg (None, [gram]) (** Command *) @@ -759,7 +759,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) = e | Vernacextend.Arg_rules rules -> let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in - let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in + let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in e in let (rpr, gpr, tpr) = arg.arg_printer in diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 0e9465839a..392f9b2ffd 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -107,13 +107,29 @@ let db_initialize = let int_of_string s = try Proofview.NonLogical.return (int_of_string s) - with e -> Proofview.NonLogical.raise e + with e -> + let e = Exninfo.capture e in + Proofview.NonLogical.raise e let string_get s i = try Proofview.NonLogical.return (String.get s i) - with e -> Proofview.NonLogical.raise e + with e -> + let e = Exninfo.capture e in + Proofview.NonLogical.raise e + +let check_positive n = + try + if n < 0 then + raise (Invalid_argument "number must be positive") + else + Proofview.NonLogical.return () + with e -> + let e = Exninfo.capture e in + Proofview.NonLogical.raise e -let run_invalid_arg () = Proofview.NonLogical.raise (Invalid_argument "run_com") +let run_invalid_arg () = + let info = Exninfo.null in + Proofview.NonLogical.raise (Invalid_argument "run_com", info) (* Gives the number of steps or next breakpoint of a run command *) let run_com inst = @@ -125,7 +141,7 @@ let run_com inst = let s = String.sub inst i (String.length inst - i) in if inst.[0] >= '0' && inst.[0] <= '9' then int_of_string s >>= fun num -> - (if num<0 then run_invalid_arg () else return ()) >> + check_positive num >> (skip:=num) >> (skipped:=0) else breakpoint:=Some (possibly_unquote s) @@ -156,11 +172,11 @@ let rec prompt level = let open Proofview.NonLogical in Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> if Util.(!batch) then return (DebugOn (level+1)) else - let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in + let exit = (skip:=0) >> (skipped:=0) >> raise (Sys.Break, Exninfo.null) in Proofview.NonLogical.catch Proofview.NonLogical.read_line begin function (e, info) -> match e with | End_of_file -> exit - | e -> raise ~info e + | e -> raise (e, info) end >>= fun inst -> match inst with @@ -176,7 +192,7 @@ let rec prompt level = Proofview.NonLogical.catch (run_com inst >> runtrue >> return (DebugOn (level+1))) begin function (e, info) -> match e with | Failure _ | Invalid_argument _ -> prompt level - | e -> raise ~info e + | e -> raise (e, info) end end diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index eabfe2f540..2d5e9e53ce 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -227,11 +227,9 @@ module PatternMatching (E:StaticEnvironment) = struct substitution. *) let wildcard_match_term = return - (** [pattern_match_term refresh pat term lhs] returns the possible - matchings of [term] with the pattern [pat => lhs]. If refresh is - true, refreshes the universes of [term]. *) - let pattern_match_term refresh pat term lhs = -(* let term = if refresh then Termops.refresh_universes_strict term else term in *) + (** [pattern_match_term pat term lhs] returns the possible + matchings of [term] with the pattern [pat => lhs]. *) + let pattern_match_term pat term lhs = match pat with | Term p -> begin @@ -262,7 +260,7 @@ module PatternMatching (E:StaticEnvironment) = struct matching rule [rule]. *) let rule_match_term term = function | All lhs -> wildcard_match_term lhs - | Pat ([],pat,lhs) -> pattern_match_term false pat term lhs + | Pat ([],pat,lhs) -> pattern_match_term pat term lhs | Pat _ -> (* Rules with hypotheses, only work in match goal. *) fail @@ -286,8 +284,7 @@ module PatternMatching (E:StaticEnvironment) = struct let hyp_match_type hypname pat hyps = pick hyps >>= fun decl -> let id = NamedDecl.get_id decl in - let refresh = is_local_def decl in - pattern_match_term refresh pat (NamedDecl.get_type decl) () <*> + pattern_match_term pat (NamedDecl.get_type decl) () <*> put_terms (id_map_try_add_name hypname (EConstr.mkVar id) empty_term_subst) <*> return id @@ -298,8 +295,8 @@ module PatternMatching (E:StaticEnvironment) = struct let hyp_match_body_and_type hypname bodypat typepat hyps = pick hyps >>= function | LocalDef (id,body,hyp) -> - pattern_match_term false bodypat body () <*> - pattern_match_term true typepat hyp () <*> + pattern_match_term bodypat body () <*> + pattern_match_term typepat hyp () <*> put_terms (id_map_try_add_name hypname (EConstr.mkVar id.binder_name) empty_term_subst) <*> return id.binder_name | LocalAssum (id,hyp) -> fail @@ -337,7 +334,7 @@ module PatternMatching (E:StaticEnvironment) = struct (* the rules are applied from the topmost one (in the concrete syntax) to the bottommost. *) let hyppats = List.rev hyppats in - pattern_match_term false conclpat concl () <*> + pattern_match_term conclpat concl () <*> hyp_pattern_list_match hyppats hyps lhs (** [match_goal hyps concl rules] matches the goal [hyps|-concl] |