diff options
Diffstat (limited to 'contrib/subtac/subtac_pretyping.ml')
| -rw-r--r-- | contrib/subtac/subtac_pretyping.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index 8dd6f9b8f..5cc735185 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -40,8 +40,11 @@ open Context open Eterm module Pretyping = Pretyping.Pretyping_F(Subtac_coercion.Coercion) + open Pretyping +let _ = Pretyping.allow_anonymous_refs := true + type recursion_info = { arg_name: name; arg_type: types; (* A *) |