diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:06:42 +0000 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:06:42 +0000 |
commit | 1117d2e4a00debfbfa0157cc3e780916df72c26b (patch) | |
tree | d8713b1126725f216e1d5ff1dcc9561d84069145 /theory.ml | |
parent | 17564e4922acda6b72bf39de7a8c23ed0c0178f6 (diff) |
New upstream version 8.6
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 |