diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 308896f3a..a87debeff 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -9,7 +9,7 @@ open CErrors open Util open Names -open Term +open Constr open Termops open Univ open Evd @@ -339,7 +339,7 @@ struct type 'a member = | App of 'a app_node - | Case of Term.case_info * 'a * 'a array * Cst_stack.t + | Case of case_info * 'a * 'a array * Cst_stack.t | Proj of int * int * projection * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t |