From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 24 Nov 2004 13:17:39 +0000 (+0000)
Subject: use get_obj instead of get_cooked_obj in order to retrieve params for
X-Git-Tag: PRE_UNIVERSES~15
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a0b3f70f4dee78cc07baf2e78673b8b7cf573995;p=helm.git

use get_obj instead of get_cooked_obj in order to retrieve params for
unchecked objects (fixes "not found" bug when trust in the environment
is false)
---

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 17ee01b53..c718524fc 100644
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -202,7 +202,8 @@ prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ;
         with
          Not_found ->
           let params =
-           (match CicEnvironment.get_cooked_obj ~trust:true uri with
+           let obj = CicEnvironment.get_obj uri in
+           (match obj with
                C.Constant _ -> raise ReferenceToConstant
              | C.Variable (_,_,_,params) -> params
              | C.CurrentProof _ -> raise ReferenceToCurrentProof
@@ -250,7 +251,8 @@ prerr_endline "---- END\n\n " ;
     | C.Appl _ -> assert false
     | C.Const (uri,exp_named_subst')  ->
        let params =
-        (match CicEnvironment.get_cooked_obj ~trust:true uri with
+        let obj = CicEnvironment.get_obj uri in
+        (match obj with
             C.Constant (_,_,_,params) -> params
           | C.Variable _ -> raise ReferenceToVariable
           | C.CurrentProof (_,_,_,_,params) -> params
@@ -263,7 +265,8 @@ prerr_endline "---- END\n\n " ;
          C.Const (uri,exp_named_subst'')
     | C.MutInd (uri,typeno,exp_named_subst') ->
        let params =
-        (match CicEnvironment.get_cooked_obj ~trust:true uri with
+        let obj = CicEnvironment.get_obj uri in
+        (match obj with
             C.Constant _ -> raise ReferenceToConstant
           | C.Variable _ -> raise ReferenceToVariable
           | C.CurrentProof _ -> raise ReferenceToCurrentProof
@@ -276,7 +279,8 @@ prerr_endline "---- END\n\n " ;
          C.MutInd (uri,typeno,exp_named_subst'')
     | C.MutConstruct (uri,typeno,consno,exp_named_subst') ->
        let params =
-        (match CicEnvironment.get_cooked_obj ~trust:true uri with
+        let obj = CicEnvironment.get_obj uri in
+        (match obj with
             C.Constant _ -> raise ReferenceToConstant
           | C.Variable _ -> raise ReferenceToVariable
           | C.CurrentProof _ -> raise ReferenceToCurrentProof