diff options
Diffstat (limited to 'contrib/correctness/past.mli')
| -rw-r--r-- | contrib/correctness/past.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli index 3c5a56c1d..b761da60e 100644 --- a/contrib/correctness/past.mli +++ b/contrib/correctness/past.mli @@ -14,10 +14,11 @@ open Names open Ptype +open Topconstr type termination = | RecArg of int - | Wf of Coqast.t * Coqast.t + | Wf of constr_expr * constr_expr type variable = identifier @@ -43,7 +44,7 @@ type ('a, 'b) t = { desc : ('a, 'b) t_desc; pre : 'b Ptype.precondition list; post : 'b Ptype.postcondition option; - loc : Coqast.loc; + loc : Util.loc; info : 'a } @@ -73,7 +74,7 @@ and ('a, 'b) arg = | Refarg of variable | Type of 'b Ptype.ml_type_v -type program = (unit, Coqast.t) t +type program = (unit, Topconstr.constr_expr) t (*s Intermediate type for CC terms. *) |