From 48a9ef28943252488e7138a8f570eef965744ee3 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 6 Dec 2011 16:13:11 +0000 Subject: [PATCH] Fixes a bug that overwrited the index of the recursive occurrence of a CoFix, causing the resulting term to always use the first corecursive definition of the same block. --- matita/components/grafite_engine/grafiteEngine.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index d3da51af0..b1e0f4c85 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -538,7 +538,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = (match spec with | NReference.Def _ -> NReference.Def height | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height) - | NReference.CoFix _ -> NReference.CoFix height + | NReference.CoFix i -> NReference.CoFix i | NReference.Ind _ | NReference.Con _ | NReference.Decl as s -> s)) | t -> NCicUtils.map status (fun _ () -> ()) () fix t @@ -605,9 +605,10 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = ) status boxml in let _,_,_,_,nobj = obj in let status = match nobj with - NCic.Inductive (is_ind,leftno,[it],_) -> - let _,ind_name,ty,cl = it in - List.fold_left + NCic.Inductive (is_ind,leftno,itl,_) -> + List.fold_left (fun status it -> + (let _,ind_name,ty,cl = it in + List.fold_left (fun status outsort -> let status = status#set_ng_mode `ProofMode in try @@ -626,7 +627,8 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let status = status#set_ng_mode `CommandMode in status) status (NCic.Prop:: - List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ())) + List.map (fun s -> NCic.Type s) + (NCicEnvironment.get_universes ())))) status itl | _ -> status in let status = match nobj with -- 2.39.2