From 19a2dd5cfbd72defe932656a65ab9da9f4ac9d1e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 31 Oct 2016 20:25:28 +0100 Subject: Moving unused code out of the kernel into Termops. Strangely enough, the checker seems to rely on an outdated decompose_app function which is not the same as the kernel, as the latter is sensitive to casts. Cast-manipulating functions from the kernel are only used on upper layers, and thus was moved there. --- plugins/quote/quote.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/quote') diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index b3ea4335f..6405c8ceb 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -183,7 +183,7 @@ type inversion_scheme = { let i_can't_do_that () = error "Quote: not a simple fixpoint" -let decomp_term c = kind_of_term (strip_outer_cast c) +let decomp_term c = kind_of_term (Termops.strip_outer_cast c) (*s [compute_lhs typ i nargsi] builds the term \texttt{(C ?nargsi ... ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive -- cgit v1.2.3