diff options
Diffstat (limited to 'theory.ml')
| -rw-r--r-- | theory.ml | 8 |
1 files changed, 4 insertions, 4 deletions
@@ -289,10 +289,10 @@ module Unit = struct end let anomaly msg = - Errors.anomaly ~label:"aac_tactics" (Pp.str msg) + CErrors.anomaly ~label:"aac_tactics" (Pp.str msg) let user_error msg = - Errors.error ("aac_tactics: " ^ msg) + CErrors.error ("aac_tactics: " ^ msg) module Trans = struct @@ -877,11 +877,11 @@ module Trans = struct t , get ( ) (** [raw_constr_of_t] rebuilds a term in the raw representation *) - let raw_constr_of_t ir rlt (context:rel_context) t = + let raw_constr_of_t ir rlt (context:Context.Rel.t) t = (** cap rebuilds the products in front of the constr *) let rec cap c = function [] -> c | t::q -> - let i = Context.lookup_rel t context in + let i = Context.Rel.lookup t context in cap (mkProd_or_LetIn i c) q in let t,indices = raw_constr_of_t_debruijn ir t in |