diff options
Diffstat (limited to 'plugins/ltac/taccoerce.ml')
| -rw-r--r-- | plugins/ltac/taccoerce.ml | 38 |
1 files changed, 20 insertions, 18 deletions
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 3812a2ba..026c00b8 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -12,9 +12,11 @@ open Util open Names open Constr open EConstr -open Misctypes +open Namegen +open Tactypes open Genarg open Stdarg +open Tacarg open Geninterp open Pp @@ -163,8 +165,7 @@ let coerce_var_to_ident fresh env sigma v = (* Interprets, if possible, a constr to an identifier which may not be fresh but suitable to be given to the fresh tactic. Works for vars, constants, inductive, constructors and sorts. *) -let coerce_to_ident_not_fresh env sigma v = -let g = sigma in +let coerce_to_ident_not_fresh sigma v = let id_of_name = function | Name.Anonymous -> Id.of_string "x" | Name.Name x -> x in @@ -181,9 +182,9 @@ let id_of_name = function | Some c -> match EConstr.kind sigma c with | Var id -> id - | Meta m -> id_of_name (Evd.meta_name g m) + | Meta m -> id_of_name (Evd.meta_name sigma m) | Evar (kn,_) -> - begin match Evd.evar_ident kn g with + begin match Evd.evar_ident kn sigma with | None -> fail () | Some id -> id end @@ -197,15 +198,16 @@ let id_of_name = function let basename = Nametab.basename_of_global ref in basename | Sort s -> - begin + begin match ESorts.kind sigma s with - | Sorts.Prop _ -> Label.to_id (Label.make "Prop") - | Sorts.Type _ -> Label.to_id (Label.make "Type") - end + | Sorts.Prop -> Label.to_id (Label.make "Prop") + | Sorts.Set -> Label.to_id (Label.make "Set") + | Sorts.Type _ -> Label.to_id (Label.make "Type") + end | _ -> fail() -let coerce_to_intro_pattern env sigma v = +let coerce_to_intro_pattern sigma v = if has_type v (topwit wit_intro_pattern) then (out_gen (topwit wit_intro_pattern) v).CAst.v else if has_type v (topwit wit_var) then @@ -218,8 +220,8 @@ let coerce_to_intro_pattern env sigma v = IntroNaming (IntroIdentifier (destVar sigma c)) | _ -> raise (CannotCoerceTo "an introduction pattern") -let coerce_to_intro_pattern_naming env sigma v = - match coerce_to_intro_pattern env sigma v with +let coerce_to_intro_pattern_naming sigma v = + match coerce_to_intro_pattern sigma v with | IntroNaming pat -> pat | _ -> raise (CannotCoerceTo "a naming introduction pattern") @@ -252,7 +254,7 @@ let coerce_to_constr env v = (try [], constr_of_id env id with Not_found -> fail ()) else fail () -let coerce_to_uconstr env v = +let coerce_to_uconstr v = if has_type v (topwit wit_uconstr) then out_gen (topwit wit_uconstr) v else @@ -296,11 +298,11 @@ let coerce_to_constr_list env v = List.map map l | None -> raise (CannotCoerceTo "a term list") -let coerce_to_intro_pattern_list ?loc env sigma v = +let coerce_to_intro_pattern_list ?loc sigma v = match Value.to_list v with | None -> raise (CannotCoerceTo "an intro pattern list") | Some l -> - let map v = CAst.make ?loc @@ coerce_to_intro_pattern env sigma v in + let map v = CAst.make ?loc @@ coerce_to_intro_pattern sigma v in List.map map l let coerce_to_hyp env sigma v = @@ -325,7 +327,7 @@ let coerce_to_hyp_list env sigma v = | None -> raise (CannotCoerceTo "a variable list") (* Interprets a qualified name *) -let coerce_to_reference env sigma v = +let coerce_to_reference sigma v = match Value.to_constr v with | Some c -> begin @@ -353,7 +355,7 @@ let coerce_to_quantified_hypothesis sigma v = (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) -let coerce_to_decl_or_quant_hyp env sigma v = +let coerce_to_decl_or_quant_hyp sigma v = if has_type v (topwit wit_int) then AnonHyp (out_gen (topwit wit_int) v) else @@ -365,7 +367,7 @@ let coerce_to_int_or_var_list v = match Value.to_list v with | None -> raise (CannotCoerceTo "an int list") | Some l -> - let map n = ArgArg (coerce_to_int n) in + let map n = Locus.ArgArg (coerce_to_int n) in List.map map l (** Abstract application, to print ltac functions *) |