use get_obj instead of get_cooked_obj in order to retrieve params for

[helm.git] / helm / ocaml / cic_proof_checking / cicSubstitution.ml

diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
index 704a8325ad806803c99f3990726e772fd794b4c5..c718524fc3b6d3e099a1eb64f45f7d6838fa51db 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml
+++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml
@@ -54,7 +54,7 @@ let lift n =
        in
         C.Meta(i,l')
     | C.Sort _ as t -> t
-    | C.Implicit as t -> t
+    | C.Implicit _ as t -> t
     | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t)
@@ -126,7 +126,7 @@ let subst arg =
        in
         C.Meta(i,l')
     | C.Sort _ as t -> t
-    | C.Implicit as t -> t
+    | C.Implicit _ as t -> t
     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
@@ -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
@@ -234,7 +235,7 @@ prerr_endline "---- END\n\n " ;
        in
         C.Meta(i,l')
     | C.Sort _ as t -> t
-    | C.Implicit as t -> t
+    | C.Implicit _ as t -> t
     | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t)
@@ -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
@@ -370,7 +374,7 @@ let lift_meta l t =
        in
         C.Meta(i,l')
     | C.Sort _ as t -> t
-    | C.Implicit as t -> t
+    | C.Implicit _ as t -> t
     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) (*CSC ??? *)
     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k + 1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k + 1) t)