From 6c3502f791a8570c61a5b2fbaf3195f373d805c8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 30 Oct 2002 18:52:44 +0000 Subject: [PATCH] Bug fixed in reduction/simplification of explicit named substitution. --- helm/gTopLevel/proofEngineReduction.ml | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 0446132c5..21f2cbebf 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -444,7 +444,7 @@ let reduce context = in if l = [] then t' else C.Appl (t'::l) and reduceaux_exp_named_subst context l = - List.map (function uri,t -> uri,reduceaux context l t) + List.map (function uri,t -> uri,reduceaux context [] t) in reduceaux context [] ;; @@ -604,11 +604,8 @@ let simpl context = if l = [] then t' else C.Appl (t'::l) end | C.Constant (_,None,_,_) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - let t' = C.Const (uri,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) + let t' = C.Const (uri,exp_named_subst') in + if l = [] then t' else C.Appl (t'::l) | C.Variable _ -> raise ReferenceToVariable | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition @@ -739,7 +736,7 @@ let simpl context = in if l = [] then t' else C.Appl (t'::l) and reduceaux_exp_named_subst context l = - List.map (function uri,t -> uri,reduceaux context l t) + List.map (function uri,t -> uri,reduceaux context [] t) in reduceaux context [] ;; -- 2.39.2