diff options
-rw-r--r-- | dev/top_printers.ml | 4 | ||||
-rw-r--r-- | grammar/argextend.ml4 | 1 | ||||
-rw-r--r-- | grammar/q_coqast.ml4 | 1 | ||||
-rw-r--r-- | interp/constrarg.ml | 4 | ||||
-rw-r--r-- | lib/genarg.ml | 13 | ||||
-rw-r--r-- | lib/genarg.mli | 2 | ||||
-rw-r--r-- | parsing/pcoq.ml | 4 | ||||
-rw-r--r-- | printing/pptactic.ml | 9 | ||||
-rw-r--r-- | tactics/tacintern.ml | 3 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 14 | ||||
-rw-r--r-- | tactics/tacsubst.ml | 3 |
11 files changed, 19 insertions, 39 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index cbebcdfcd..cc1cf23d6 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -510,7 +510,7 @@ let _ = try Vernacinterp.vinterp_add false ("PrintConstr", 0) (function - [c] when genarg_tag c = ConstrArgType && true -> + [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in (fun () -> in_current_context constr_display c) | _ -> failwith "Vernac extension: cannot occur") @@ -526,7 +526,7 @@ let _ = try Vernacinterp.vinterp_add false ("PrintPureConstr", 0) (function - [c] when genarg_tag c = ConstrArgType && true -> + [c] when genarg_tag c = unquote (topwit wit_constr) && true -> let c = out_gen (rawwit wit_constr) c in (fun () -> in_current_context print_pure_constr c) | _ -> failwith "Vernac extension: cannot occur") diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 9abe5d7cf..cb006186a 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -30,7 +30,6 @@ let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >> let rec make_wit loc = function - | ConstrArgType -> <:expr< Constrarg.wit_constr >> | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >> | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >> | PairArgType (t1,t2) -> diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 798d428e9..e11b37fc0 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -223,7 +223,6 @@ let mlexpr_of_red_expr = function <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >> let rec mlexpr_of_argtype loc = function - | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >> | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >> | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >> | Genarg.PairArgType (t1,t2) -> diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 94c13fe79..a8dfd02e1 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -44,7 +44,8 @@ let wit_quant_hyp = Genarg.make0 None "quant_hyp" let wit_sort : (glob_sort, glob_sort, sorts) genarg_type = Genarg.make0 None "sort" -let wit_constr = unsafe_of_type ConstrArgType +let wit_constr = + Genarg.make0 None "constr" let wit_constr_may_eval = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "constr_may_eval" @@ -75,6 +76,7 @@ let () = register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern"; register_name0 wit_tactic "Constrarg.wit_tactic"; register_name0 wit_sort "Constrarg.wit_sort"; + register_name0 wit_constr "Constrarg.wit_constr"; register_name0 wit_uconstr "Constrarg.wit_uconstr"; register_name0 wit_open_constr "Constrarg.wit_open_constr"; register_name0 wit_constr_may_eval "Constrarg.wit_constr_may_eval"; diff --git a/lib/genarg.ml b/lib/genarg.ml index af9ea70ec..c2c1014f1 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -57,14 +57,12 @@ end type argument_type = (* Specific types *) - | ConstrArgType | ListArgType of argument_type | OptArgType of argument_type | PairArgType of argument_type * argument_type | ExtraArgType of string let rec argument_type_eq arg1 arg2 = match arg1, arg2 with -| ConstrArgType, ConstrArgType -> true | ListArgType arg1, ListArgType arg2 -> argument_type_eq arg1 arg2 | OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2 | PairArgType (arg1l, arg1r), PairArgType (arg2l, arg2r) -> @@ -73,7 +71,6 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with | _ -> false let rec pr_argument_type = function -| ConstrArgType -> str "constr" | ListArgType t -> pr_argument_type t ++ spc () ++ str "list" | OptArgType t -> pr_argument_type t ++ spc () ++ str "opt" | PairArgType (t1, t2) -> @@ -190,19 +187,12 @@ let default_empty_value t = | _ -> None) | ExtraArgType s -> (String.Map.find s !arg0_map).nil - | _ -> None in + in match aux t with | Some v -> Some (Obj.obj v) | None -> None -(** Beware: keep in sync with the corresponding types *) -let base_create n = Val.Base (Dyn.create n) -let genarg_T = base_create "genarg" -let constr_T = base_create "constr" - let rec val_tag = function - (** Must ensure that toplevel types of Var and Ident agree! *) -| ConstrArgType -> cast_tag constr_T | ExtraArgType s -> cast_tag (String.Map.find s !arg0_map).dyn | ListArgType t -> cast_tag (Val.List (val_tag t)) | OptArgType t -> cast_tag (Val.Opt (val_tag t)) @@ -222,7 +212,6 @@ let try_prj wit v = match prj (val_tag wit) v with let rec val_cast : type a. a typed_abstract_argument_type -> Val.t -> a = fun wit v -> match unquote wit with -| ConstrArgType | ExtraArgType _ -> try_prj wit v | ListArgType t -> let Val.Dyn (tag, v) = v in diff --git a/lib/genarg.mli b/lib/genarg.mli index 8d929f9f6..56c09f14f 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -211,8 +211,6 @@ val val_cast : 'a typed_abstract_argument_type -> Val.t -> 'a (** {6 Type reification} *) type argument_type = - (** Basic types *) - | ConstrArgType (** Specific types *) | ListArgType of argument_type | OptArgType of argument_type diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index df0d26206..3ed530425 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -272,7 +272,7 @@ let create_entry u s etyp = new_entry etyp u s let create_constr_entry s = - outGramObj (rawwit wit_constr) (create_entry uconstr s ConstrArgType) + outGramObj (rawwit wit_constr) (create_entry uconstr s (unquote (rawwit wit_constr))) let create_generic_entry s wit = outGramObj wit (create_entry utactic s (unquote wit)) @@ -633,7 +633,7 @@ let compute_entry allow_create adjust forpat = function let u = get_univ u in let e = try get_entry u n - with Not_found when allow_create -> create_entry u n ConstrArgType in + with Not_found when allow_create -> create_entry u n (unquote (rawwit wit_constr)) in object_of_typed_entry e, None, true (* This computes the name of the level where to add a new rule *) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index df5f57dac..a8fa8313f 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -267,7 +267,6 @@ module Make let rec pr_raw_generic_rec prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) = match Genarg.genarg_tag x with - | ConstrArgType -> prc (out_gen (rawwit wit_constr) x) | ListArgType _ -> let list_unpacker wit l = let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in @@ -295,7 +294,6 @@ module Make let rec pr_glb_generic_rec prc prlc prtac prpat x = match Genarg.genarg_tag x with - | ConstrArgType -> prc (out_gen (glbwit wit_constr) x) | ListArgType _ -> let list_unpacker wit l = let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in @@ -322,7 +320,6 @@ module Make let rec pr_top_generic_rec prc prlc prtac prpat x = match Genarg.genarg_tag x with - | ConstrArgType -> prc (out_gen (topwit wit_constr) x) | ListArgType _ -> let list_unpacker wit l = let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in @@ -1427,6 +1424,12 @@ let () = Genprint.register_print0 Constrarg.wit_sort pr_glob_sort pr_glob_sort (pr_sort Evd.empty); Genprint.register_print0 + Constrarg.wit_constr + Ppconstr.pr_constr_expr + (fun (c, _) -> Printer.pr_glob_constr c) + Printer.pr_constr + ; + Genprint.register_print0 Constrarg.wit_uconstr Ppconstr.pr_constr_expr (fun (c,_) -> Printer.pr_glob_constr c) diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index ac0c4b266..6f6c4a05a 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -720,8 +720,6 @@ and intern_match_rule onlytac ist = function and intern_genarg ist x = match genarg_tag x with - | ConstrArgType -> - map_raw wit_constr intern_constr ist x | ListArgType _ -> let list_unpacker wit l = let map x = @@ -830,6 +828,7 @@ let () = Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); Genintern.register_intern0 wit_sort (fun ist s -> (ist, s)); Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis); + Genintern.register_intern0 wit_constr (fun ist c -> (ist,intern_constr ist c)); Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c)); Genintern.register_intern0 wit_open_constr (fun ist c -> (ist,intern_constr ist c)); Genintern.register_intern0 wit_red_expr (lift intern_red_expr); diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index adca22630..71a6e043b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1522,18 +1522,9 @@ and interp_genarg ist x : Val.t Ftactic.t = let tag = genarg_tag x in if argument_type_eq tag (unquote (topwit (wit_list wit_var))) then interp_genarg_var_list ist x - else match tag with - | ConstrArgType -> - Ftactic.nf_s_enter { s_enter = begin fun gl -> - let c = Genarg.out_gen (glbwit wit_constr) x in - let env = Proofview.Goal.env gl in - let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in - let (sigma, c) = interp_constr ist env sigma c in - let c = in_gen (topwit wit_constr) c in - Sigma.Unsafe.of_pair (Ftactic.return c, sigma) - end } - | ListArgType ConstrArgType -> + else if argument_type_eq tag (unquote (topwit (wit_list wit_constr))) then interp_genarg_constr_list ist x + else match tag with | ListArgType _ -> let list_unpacker wit l = let map x = @@ -2184,6 +2175,7 @@ let () = Geninterp.register_interp0 wit_var (lift interp_hyp); Geninterp.register_interp0 wit_intro_pattern (lifts interp_intro_pattern); Geninterp.register_interp0 wit_clause_dft_concl (lift interp_clause); + Geninterp.register_interp0 wit_constr (lifts interp_constr); Geninterp.register_interp0 wit_sort (lifts (fun _ _ evd s -> interp_sort evd s)); Geninterp.register_interp0 wit_tacvalue (fun ist v -> Ftactic.return v); Geninterp.register_interp0 wit_red_expr (lifts interp_red_expr); diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 0061237bf..4f7911524 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -276,8 +276,6 @@ and subst_match_rule subst = function and subst_genarg subst (x:glob_generic_argument) = match genarg_tag x with - | ConstrArgType -> - in_gen (glbwit wit_constr) (subst_glob_constr subst (out_gen (glbwit wit_constr) x)) | ListArgType _ -> let list_unpacker wit l = let map x = @@ -315,6 +313,7 @@ let () = Genintern.register_subst0 wit_var (fun _ v -> v); Genintern.register_subst0 wit_intro_pattern (fun _ v -> v); Genintern.register_subst0 wit_tactic subst_tactic; + Genintern.register_subst0 wit_constr subst_glob_constr; Genintern.register_subst0 wit_sort (fun _ v -> v); Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v); Genintern.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c); |