diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/extraargs.mlg | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.mlg | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 15 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.ml | 3 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 |
5 files changed, 11 insertions, 13 deletions
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index 2654729652..e6e6e29d4f 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -332,7 +332,7 @@ END let local_test_lpar_id_colon = let err () = raise Stream.Failure in Pcoq.Entry.of_parser "lpar_id_colon" - (fun strm -> + (fun _ strm -> match Util.stream_nth 0 strm with | Tok.KEYWORD "(" -> (match Util.stream_nth 1 strm with diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 5c84b35f1b..cab8ed0a55 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -64,7 +64,7 @@ let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode (* Hack to parse "[ id" without dropping [ *) let test_bracket_ident = Pcoq.Entry.of_parser "test_bracket_ident" - (fun strm -> + (fun _ strm -> match stream_nth 0 strm with | KEYWORD "[" -> (match stream_nth 1 strm with diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 945a2dd613..9b52b710c1 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -24,7 +24,6 @@ open Tactypes open Tactics open Inv open Locus -open Decl_kinds open Pcoq @@ -40,7 +39,7 @@ let err () = raise Stream.Failure (* admissible notation "(x t)" *) let test_lpar_id_coloneq = Pcoq.Entry.of_parser "lpar_id_coloneq" - (fun strm -> + (fun _ strm -> match stream_nth 0 strm with | KEYWORD "(" -> (match stream_nth 1 strm with @@ -54,7 +53,7 @@ let test_lpar_id_coloneq = (* Hack to recognize "(x)" *) let test_lpar_id_rpar = Pcoq.Entry.of_parser "lpar_id_coloneq" - (fun strm -> + (fun _ strm -> match stream_nth 0 strm with | KEYWORD "(" -> (match stream_nth 1 strm with @@ -68,7 +67,7 @@ let test_lpar_id_rpar = (* idem for (x:=t) and (1:=t) *) let test_lpar_idnum_coloneq = Pcoq.Entry.of_parser "test_lpar_idnum_coloneq" - (fun strm -> + (fun _ strm -> match stream_nth 0 strm with | KEYWORD "(" -> (match stream_nth 1 strm with @@ -85,7 +84,7 @@ open Extraargs (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *) let check_for_coloneq = Pcoq.Entry.of_parser "lpar_id_colon" - (fun strm -> + (fun _ strm -> let rec skip_to_rpar p n = match List.last (Stream.npeek n strm) with | KEYWORD "(" -> skip_to_rpar (p+1) (n+1) @@ -109,7 +108,7 @@ let check_for_coloneq = let lookup_at_as_comma = Pcoq.Entry.of_parser "lookup_at_as_comma" - (fun strm -> + (fun _ strm -> match stream_nth 0 strm with | KEYWORD (","|"at"|"as") -> () | _ -> err ()) @@ -450,9 +449,9 @@ GRAMMAR EXTEND Gram | -> { true } ] ] ; simple_binder: - [ [ na=name -> { ([na],Default Explicit, CAst.make ~loc @@ + [ [ na=name -> { ([na],Default Glob_term.Explicit, CAst.make ~loc @@ CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) } - | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Explicit,c) } + | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Glob_term.Explicit,c) } ] ] ; fixdecl: diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 0e38ce575b..6df068883c 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -20,7 +20,6 @@ open Stdarg open Notation_gram open Tactypes open Locus -open Decl_kinds open Genredexpr open Ppconstr open Pputils @@ -1097,7 +1096,7 @@ let pr_goal_selector ~toplevel s = let rec strip_ty acc n ty = if Int.equal n 0 then (List.rev acc, (ty,None)) else match DAst.get ty with - Glob_term.GProd(na,Explicit,a,b) -> + Glob_term.GProd(na,Glob_term.Explicit,a,b) -> strip_ty (([CAst.make na],(a,None))::acc) (n-1) b | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 726752a2bf..1493092f2f 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -546,7 +546,7 @@ let rewrite_core_unif_flags = { Unification.check_applied_meta_types = true; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; - Unification.frozen_evars = Evar.Set.empty; + Unification.allowed_evars = Unification.AllowAll; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; Unification.modulo_eta = true; |