From 45e1e0dcba3101b6a9e096f18c28da899615af7f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 May 2018 08:40:25 +0200 Subject: Fix the checker by merely adapting the data structure. Unluckily, this is completely wrong as we trust the inlined term to be well-typed in some unavailable environment. To start with, the checker should not even rely on substitutions as it does not trust functors, but it does anyways. I have thus commented this code as a useful backdoor for when Coq is used to implement the next blockchain Ponzi scheme. We really need to sort this out though. --- checker/cic.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker/cic.mli') diff --git a/checker/cic.mli b/checker/cic.mli index 27e2a479f..7ec345768 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -128,7 +128,7 @@ type section_context = unit (** {6 Substitutions} *) type delta_hint = - | Inline of int * constr option + | Inline of int * (Univ.AUContext.t * constr) option | Equiv of KerName.t type delta_resolver = ModPath.t MPmap.t * delta_hint KNmap.t -- cgit v1.2.3