From c036cf8b560ad40dbc06e94530af938e6f994aca Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 10 Mar 2008 13:25:42 +0000 Subject: [PATCH] whd: ~delta=false now controls also zeta-reduction. This greatly speed-ups some operations when definitions are in the context. Moreover, the semantics seems more reasonable (????). --- .../cic_proof_checking/cicReduction.ml | 28 ++++++++++--------- 1 file changed, 15 insertions(+), 13 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 7f1ec5835..532d0dc1e 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.ml +++ b/helm/software/components/cic_proof_checking/cicReduction.ml @@ -596,19 +596,21 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; function (k, e, _, C.Rel n, s) as config -> let config' = - try - Some (RS.from_env (List.nth e (n-1))) - with - Failure _ -> - try - begin - match List.nth context (n - 1 - k) with - None -> assert false - | Some (_,C.Decl _) -> None - | Some (_,C.Def (x,_)) -> Some (0,[],[],S.lift (n - k) x,[]) - end - with - Failure _ -> None + if not delta then None + else + try + Some (RS.from_env (List.nth e (n-1))) + with + Failure _ -> + try + begin + match List.nth context (n - 1 - k) with + None -> assert false + | Some (_,C.Decl _) -> None + | Some (_,C.Def (x,_)) -> Some (0,[],[],S.lift (n - k) x,[]) + end + with + Failure _ -> None in (match config' with Some (k',e',ens',t',s') -> reduce (k',e',ens',t',s'@s) -- 2.39.2