diff options
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 2d4e8a903..6a12e8d35 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -10,6 +10,7 @@ open Term open Sign open Environ open Reduction +open Inductive open Typing open Proof_trees open Proof_type @@ -23,7 +24,7 @@ type refiner_error = | OccurMeta of constr | CannotApply of constr * constr | CannotUnify of constr * constr - | CannotGeneralize of typed_type signature * constr + | CannotGeneralize of constr | NotWellTyped of constr | BadTacticArgs of string * tactic_arg list |