From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 7 Jun 2005 15:44:16 +0000 (+0000)
Subject: added whd to match argument in guarded_by_destructors;
X-Git-Tag: PRE_INDEX_1~58
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=055981b13cb4222632a46dbdf07859f522569d52;p=helm.git

added whd to match argument in guarded_by_destructors;
before only verbatim occurrences of safe variables were accepted.
---

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 9f5b280af..fbcf25f91 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -903,7 +903,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
        (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
        exp_named_subst true
    | C.MutCase (uri,i,outtype,term,pl) ->
-      (match term with
+      (match CicReduction.whd context term with
           C.Rel m when List.mem m safes || m = x ->
            let (tys,len,isinductive,paramsno,cl) =
 	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in