diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.ml | 1 | ||||
| -rw-r--r-- | proofs/evar_refiner.mli | 1 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 1 |
3 files changed, 3 insertions, 0 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 48fa2202ee..d38ff7512f 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -14,6 +14,7 @@ open Evarutil open Evarsolve open Pp open Glob_term +open Ltac_pretype (******************************************) (* Instantiation of existential variables *) diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 5d69715967..a0e3b718a2 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -8,6 +8,7 @@ open Evd open Glob_term +open Ltac_pretype (** Refinement of existential variables. *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 7e6d83b10f..d4e9555f34 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -15,6 +15,7 @@ open Proof_type open Redexpr open Pattern open Locus +open Ltac_pretype (** Operations for handling terms under a local typing context. *) |