diff options
| author | Maxime Dénès | 2017-10-27 18:18:30 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-27 18:18:30 +0200 |
| commit | ff4793c609d4fc2b868ff673ffaa48abf6d5fa03 (patch) | |
| tree | 49a7a2cf4ebe5cd0066156a096434f3014f0fd06 /proofs | |
| parent | 99b1f939f8ca56b328a159c27033052c6fcb9a81 (diff) | |
| parent | bf4112094feb1a705d8bdaea3fb0febc4ef3ff59 (diff) | |
Merge PR #6015: [general] Remove Econstr dependency from `intf`
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. *) |