From 1117d2e4a00debfbfa0157cc3e780916df72c26b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:06:42 +0000 Subject: New upstream version 8.6 --- theory.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'theory.ml') diff --git a/theory.ml b/theory.ml index a5229fa..20cb299 100644 --- a/theory.ml +++ b/theory.ml @@ -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 -- cgit v1.2.3