Added module DiscriminationTactics with brand new tactics Injection and

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

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index f7ddd1968047db0a87abba9954140be3762cbd10..581c5918f4c78c301c1ba65009cc48aa2fc222da 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -57,7 +57,7 @@ let whd context =
         | None -> raise RelToHiddenHypothesis
        )
     | C.Var (uri,exp_named_subst) as t ->
-       (match CicEnvironment.get_cooked_obj uri with
+       (match CicEnvironment.get_cooked_obj ~trust:false uri with
            C.Constant _ -> raise ReferenceToConstant
          | C.CurrentProof _ -> raise ReferenceToCurrentProof
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
@@ -80,7 +80,7 @@ let whd context =
     | C.Appl (he::tl) -> whdaux (tl@l) he
     | C.Appl [] -> raise (Impossible 1)
     | C.Const (uri,exp_named_subst) as t ->
-       (match CicEnvironment.get_cooked_obj uri with
+       (match CicEnvironment.get_cooked_obj ~trust:false uri with
            C.Constant (_,Some body,_,_) ->
             whdaux l (CicSubstitution.subst_vars exp_named_subst body)
          | C.Constant _ -> if l = [] then t else C.Appl (t::l)