diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index ca3bd1e802..a8debc6fd6 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 -> - (var_map * unbound_ltac_var_map) * rawconstr -> evar_map -> evar_map + rawconstr_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/proof_type.ml b/proofs/proof_type.ml index 55a73c608b..27b186a82a 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -96,7 +96,7 @@ type ltac_call_kind = | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref | LtacVarCall of identifier * glob_tactic_expr | LtacConstrInterp of rawconstr * - ((identifier * constr) list * (identifier * identifier option) list) + (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 b07389ceee..73be0c2b7a 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -126,7 +126,7 @@ type ltac_call_kind = | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref | LtacVarCall of identifier * glob_tactic_expr | LtacConstrInterp of rawconstr * - ((identifier * constr) list * (identifier * identifier option) list) + (extended_patvar_map * (identifier * identifier option) list) type ltac_trace = (int * loc * ltac_call_kind) list |