diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/evar_refiner.mli | 2 | ||||
| -rw-r--r-- | proofs/goal.ml | 2 | ||||
| -rw-r--r-- | proofs/goal.mli | 4 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 2 | ||||
| -rw-r--r-- | proofs/tacexpr.ml | 14 | ||||
| -rw-r--r-- | proofs/tactic_debug.mli | 4 |
8 files changed, 16 insertions, 16 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index e1d41b960..43c7e6e5a 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -43,7 +43,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = try Pretyping.Default.understand_ltac true sigma env ltac_var (Pretyping.OfType (Some evi.evar_concl)) rawc with _ -> - let loc = Rawterm.loc_of_rawconstr rawc in + let loc = Rawterm.loc_of_glob_constr rawc in user_err_loc (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^ string_of_existential evk)) diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 7ce8a54c4..b800d0d66 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -17,7 +17,7 @@ open Rawterm (** Refinement of existential variables. *) val w_refine : evar * evar_info -> - rawconstr_ltac_closure -> evar_map -> evar_map + glob_constr_ltac_closure -> evar_map -> evar_map val instantiate_pf_com : Evd.evar -> Topconstr.constr_expr -> Evd.evar_map -> Evd.evar_map diff --git a/proofs/goal.ml b/proofs/goal.ml index 9f0d48bb1..a48bc2945 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -175,7 +175,7 @@ module Refinable = struct asks whether the term should have the same type as the conclusion. [resolve_classes] is a flag on pretyping functions which, if set to true, calls the typeclass resolver. - The principal argument is a [rawconstr] which is then pretyped in the + The principal argument is a [glob_constr] which is then pretyped in the context of a term, the remaining evars are registered to the handle. It is the main component of the toplevel refine tactic.*) (* spiwack: it is not entirely satisfactory to have this function here. Plus it is diff --git a/proofs/goal.mli b/proofs/goal.mli index b291e1a77..3d9fcc5a2 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -69,11 +69,11 @@ module Refinable : sig The [check_type] argument asks whether the term should have the same type as the conclusion. [resolve_classes] is a flag on pretyping functions which, if set to true, calls the typeclass resolver. - The principal argument is a [rawconstr] which is then pretyped in the + The principal argument is a [glob_constr] which is then pretyped in the context of a term, the remaining evars are registered to the handle. It is the main component of the toplevel refine tactic.*) val constr_of_raw : - handle -> bool -> bool -> Rawterm.rawconstr -> Term.constr sensitive + handle -> bool -> bool -> Rawterm.glob_constr -> Term.constr sensitive end diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index ff28ba877..ebb6db213 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -94,7 +94,7 @@ type ltac_call_kind = | LtacNameCall of ltac_constant | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref | LtacVarCall of identifier * glob_tactic_expr - | LtacConstrInterp of rawconstr * + | LtacConstrInterp of glob_constr * (extended_patvar_map * (identifier * identifier option) list) type ltac_trace = (int * loc * ltac_call_kind) list diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 886c0db42..cf73e0dca 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -124,7 +124,7 @@ type ltac_call_kind = | LtacNameCall of ltac_constant | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref | LtacVarCall of identifier * glob_tactic_expr - | LtacConstrInterp of rawconstr * + | LtacConstrInterp of glob_constr * (extended_patvar_map * (identifier * identifier option) list) type ltac_trace = (int * loc * ltac_call_kind) list diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 855d2cea7..b9e22ca05 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -262,8 +262,8 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg = (* Globalized tactics *) and glob_tactic_expr = - (rawconstr_and_expr, - rawconstr_and_expr * constr_pattern, + (glob_constr_and_expr, + glob_constr_and_expr * constr_pattern, evaluable_global_reference and_short_name or_var, inductive or_var, ltac_constant located or_var, @@ -307,8 +307,8 @@ type raw_red_expr = (constr_expr, reference or_by_notation, constr_expr) red_expr_gen type glob_atomic_tactic_expr = - (rawconstr_and_expr, - rawconstr_and_expr * constr_pattern, + (glob_constr_and_expr, + glob_constr_and_expr * constr_pattern, evaluable_global_reference and_short_name or_var, inductive or_var, ltac_constant located or_var, @@ -317,8 +317,8 @@ type glob_atomic_tactic_expr = glevel) gen_atomic_tactic_expr type glob_tactic_arg = - (rawconstr_and_expr, - rawconstr_and_expr * constr_pattern, + (glob_constr_and_expr, + glob_constr_and_expr * constr_pattern, evaluable_global_reference and_short_name or_var, inductive or_var, ltac_constant located or_var, @@ -329,7 +329,7 @@ type glob_tactic_arg = type glob_generic_argument = glevel generic_argument type glob_red_expr = - (rawconstr_and_expr, evaluable_global_reference or_var, constr_pattern) + (glob_constr_and_expr, evaluable_global_reference or_var, constr_pattern) red_expr_gen type typed_generic_argument = tlevel generic_argument diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index 42d81e863..d96f4c746 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -22,7 +22,7 @@ val set_tactic_printer : (glob_tactic_expr ->Pp.std_ppcmds) -> unit val set_match_pattern_printer : (env -> constr_pattern match_pattern -> Pp.std_ppcmds) -> unit val set_match_rule_printer : - ((Genarg.rawconstr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) -> + ((Genarg.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) -> unit (** Debug information *) @@ -39,7 +39,7 @@ val db_constr : debug_info -> env -> constr -> unit (** Prints the pattern rule *) val db_pattern_rule : - debug_info -> int -> (Genarg.rawconstr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit + debug_info -> int -> (Genarg.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit (** Prints a matched hypothesis *) val db_matched_hyp : |