From a8a829deabda2ae4d64e48d455d7df3b932296ba Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 14 Feb 2006 12:40:49 +0000 Subject: [PATCH] reverted orrible but correct syntax --- helm/software/components/cic_proof_checking/cicReduction.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 5a638b5f7..56e98775f 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.ml +++ b/helm/software/components/cic_proof_checking/cicReduction.ml @@ -969,8 +969,8 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[]) = end in debug t1 [t2] "PREWHD"; - let t1' = whd ~delta:true ~subst context t1 in - let t2' = whd ~delta:true ~subst context t2 in + let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in + let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in debug t1' [t2'] "POSTWHD"; aux2 test_equality_only t1' t2' ugraph in -- 2.39.2