diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 2d07bf4d5..820a81b5d 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -18,7 +18,7 @@ open Termops open Find_subterm open Namegen open Environ -open Closure +open CClosure open Reductionops open Cbv open Patternops |