From 13ea06251e64004ad537d5c71b4082af52085ff0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Apr 2008 11:04:14 +0000 Subject: [PATCH] new constants have depth = max_int insted of 0 so that reducing to 0 expands them --- helm/software/components/ng_kernel/nCicReduction.ml | 4 ++-- helm/software/components/ng_kernel/nReference.ml | 2 +- helm/software/components/ng_kernel/oCic2NCic.ml | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 64133384d..defd12e29 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -419,11 +419,11 @@ module Reduction(RS : Strategy) = | (_, _, 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) + if delta > height then config else aux (0, [], body, s) | (_, _, NCic.Const (NReference.Ref (_,_,NReference.Fix (_,recindex)) as refer),s) as config -> let _,_,body,_, _, height = NCicEnvironment.get_checked_fix refer in - if delta >= height then config else + if delta > height then config else (match try Some (RS.from_stack (List.nth s recindex)) with Failure _ -> None diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml index 4ecf74645..2692075e0 100644 --- a/helm/software/components/ng_kernel/nReference.ml +++ b/helm/software/components/ng_kernel/nReference.ml @@ -121,7 +121,7 @@ let mk_constructor j = function let reference_of_ouri u indinfo = let u = NUri.nuri_of_ouri u in - reference_of_string (string_of_reference (Ref (~-1,u,indinfo))) + reference_of_string (string_of_reference (Ref (max_int,u,indinfo))) ;; let ouri_of_reference (Ref (_,u,_)) = NUri.ouri_of_nuri u;; diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 5bb6b93e2..f20df7c80 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -262,6 +262,6 @@ let convert_obj_aux uri = function let convert_obj uri obj = let o, fixpoints = convert_obj_aux uri obj in - let obj = NUri.nuri_of_ouri uri,0, [], [], o in + let obj = NUri.nuri_of_ouri uri,max_int, [], [], o in fixpoints @ [obj] ;; -- 2.39.2