From 086c66b6682a49fec4041c25e741b2736f385e6a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 5 Dec 2002 14:57:45 +0000 Subject: [PATCH] A simplification bug was introduced during the clean-up before the last commit. Fixed. --- helm/gTopLevel/proofEngineReduction.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 04bfe9ae5..208864c80 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -584,14 +584,16 @@ let simpl context = aux [] l (CicSubstitution.subst_vars exp_named_subst' body) in (**** Step 3 ****) - let term_to_fold = + let term_to_fold, delta_expanded_term_to_fold = let body' = CicSubstitution.subst_vars exp_named_subst' body in match constant_args with - [] -> body' - | _ -> C.Appl (body'::constant_args) + [] -> C.Const (uri,exp_named_subst'), body' + | _ -> + C.Appl ((C.Const (uri,exp_named_subst'))::constant_args), + C.Appl (body'::constant_args) in let simplified_term_to_fold = - reduceaux context [] term_to_fold + reduceaux context [] delta_expanded_term_to_fold in replace (=) simplified_term_to_fold term_to_fold res with -- 2.39.2