diff options
| author |  Matej Košík <matej.kosik@inria.fr> | 2017-05-29 11:02:06 +0200 |
|---|---|---|
| committer | Matej Košík <matej.kosik@inria.fr> | 2017-06-10 10:33:53 +0200 |
| commit | b6feaafc7602917a8ef86fb8adc9651ff765e710 (patch) | |
| tree | 5a033488c31040009adb725f20e8bd0a5dd31bc5 /plugins/ssr/ssrparser.ml4 | |
| parent | 102d7418e399de646b069924277e4baea1badaca (diff) | |
Remove (useless) aliases from the API.
Diffstat (limited to 'plugins/ssr/ssrparser.ml4')
| -rw-r--r-- | plugins/ssr/ssrparser.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 5fd377233..3ea8c2431 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1465,7 +1465,7 @@ let ssr_id_of_string loc s = else Feedback.msg_warning (str ( "The name " ^ s ^ " fits the _xxx_ format used for anonymous variables.\n" ^ "Scripts with explicit references to anonymous variables are fragile.")) - end; id_of_string s + end; Id.of_string s let ssr_null_entry = Gram.Entry.of_parser "ssr_null" (fun _ -> ()) @@ -1555,7 +1555,7 @@ END let ssrautoprop gl = try let tacname = - try Nametab.locate_tactic (qualid_of_ident (id_of_string "ssrautoprop")) + try Nametab.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop")) with Not_found -> Nametab.locate_tactic (ssrqid "ssrautoprop") in let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in Proofview.V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl @@ -2320,7 +2320,7 @@ let test_idcomma = Gram.Entry.of_parser "test_idcomma" accept_idcomma GEXTEND Gram GLOBAL: ssr_idcomma; ssr_idcomma: [ [ test_idcomma; - ip = [ id = IDENT -> Some (id_of_string id) | "_" -> None ]; "," -> + ip = [ id = IDENT -> Some (Id.of_string id) | "_" -> None ]; "," -> Some ip ] ]; END |