From a3c9916401dbaac8e59948e878eec0f37e72bf4a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 17 Jan 2006 18:21:31 +0000 Subject: [PATCH] Bug fixed (in Cast). --- helm/ocaml/tactics/proofEngineReduction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml index cc5af63ae..fca06f6f0 100644 --- a/helm/ocaml/tactics/proofEngineReduction.ml +++ b/helm/ocaml/tactics/proofEngineReduction.ml @@ -631,7 +631,7 @@ let simpl context = | C.Sort _ as t -> t (* l should be empty *) | C.Implicit _ as t -> t | C.Cast (te,ty) -> - C.Cast (reduceaux context l te, reduceaux context l ty) + C.Cast (reduceaux context l te, reduceaux context [] ty) | C.Prod (name,s,t) -> assert (l = []) ; C.Prod (name, -- 2.39.2