trust implemented, but in the nCicTypeChecker!

[helm.git] / helm / software / components / ng_kernel / nCicReduction.ml

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 0d3a265bb0efb7dda01e526630cd3c4b4f3f44cc..a825e55d58e30653a7c5d5d0bae85438aaeb7066 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -13,28 +13,6 @@
 
 (* TODO unify exceptions *)
 
-exception WrongUriToInductiveDefinition;;
-exception Impossible of int;;
-exception ReferenceToConstant;;
-exception ReferenceToVariable;;
-exception ReferenceToCurrentProof;;
-exception ReferenceToInductiveDefinition;;
-
-let debug = false
-let profile = false
-let debug_print s = if debug then prerr_endline (Lazy.force s)
-
-let fdebug = ref 1;;
-let debug t env s =
- let rec debug_aux t i =
-  let module C = Cic in
-  let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
- in
-  if !fdebug = 0 then
-   debug_print (lazy (s ^ "\n" ^ List.fold_right debug_aux (t::env) ""))
-;;
-
 module type Strategy =
  sig
   type stack_term
@@ -418,12 +396,12 @@ module Reduction(RS : Strategy) =
         in
          aux (k, e, he, tl' @ s)
      | (_, _, NCic.Const
-            (NReference.Ref (_,_,NReference.Def) as refer), s) as config ->
-         let _,_,body,_,_,height = NCicEnvironment.get_checked_def refer in
-         if delta > height then config else aux (0, [], body, s) 
+            (NReference.Ref (height,_,NReference.Def) as refer), s) as config ->
+         if delta > height then config else 
+           let _,_,body,_,_,_ = NCicEnvironment.get_checked_def refer in
+           aux (0, [], body, s) 
      | (_, _, NCic.Const (NReference.Ref 
-               (_,_,NReference.Fix (fixno,recindex)) as refer),s) as config ->
-        let fixes,_, height = NCicEnvironment.get_checked_fixes refer in
+           (height,_,NReference.Fix (fixno,recindex)) as refer),s) as config ->
         if delta > height then config else
         (match
           try Some (RS.from_stack (List.nth s recindex))
@@ -431,6 +409,7 @@ module Reduction(RS : Strategy) =
         with 
         | None -> config
         | Some recparam ->
+           let fixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in
            match reduce ~delta:0 ~subst context recparam with
            | (_,_,NCic.Const (NReference.Ref (_,_,NReference.Con _)), _) as c ->
                let new_s =
@@ -443,7 +422,7 @@ module Reduction(RS : Strategy) =
      | (k, e, NCic.Match (_,_,term,pl),s) as config ->
         let decofix = function
           | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix c)as refer),s)->
-             let cofixes,_,_ = NCicEnvironment.get_checked_cofixes refer in
+             let cofixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in
              let _,_,_,_,body = List.nth cofixes c in
              reduce ~delta:0 ~subst context (0,[],body,s)
           | config -> config