From db9beee355f93cc6403d1837dc9674d20ebce30e Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 4 Oct 2000 15:57:52 +0000 Subject: Nouvelle stratégie de nommage dans Simpl pour Fix MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@653 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/tacred.ml | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index e32520f1a..36f6c8d8d 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -66,9 +66,9 @@ let rec compute_consteval c = let nargs = List.length l in match kind_of_term c' with | IsConst cst -> - (match constant_eval cst with + (match constant_descend cst with | NotAnElimination -> raise Elimconst - | IsElimination (p,e) -> (p+n-nargs, EliminationConst e)) + | IsElimination (p,e) -> (max (p+n-nargs) n, EliminationConst e)) | IsLambda (_,t,g) when l=[] -> srec (n+1) (t::labs) g | IsFix ((lv,i),(tys,_,bds)) -> if (List.length l) > n then raise Elimconst; @@ -88,7 +88,7 @@ let rec compute_consteval c = raise Elimconst) l in if list_distinct (List.map fst li) then - (n-nargs+lv.(i), EliminationFix (li,n)) + (n-nargs+nbfix, EliminationFix (li,n)) else raise Elimconst | IsMutCase (_,_,d,_) when isRel d -> (n, EliminationCases) @@ -97,15 +97,16 @@ let rec compute_consteval c = try IsElimination (srec 0 [] c) with Elimconst -> NotAnElimination -and constant_eval (sp,_ as cst) = +and constant_descend cst = + match constant_opt_value (Global.env ()) cst with + | None -> NotAnElimination + | Some c -> compute_consteval c + +let constant_eval (sp,_ as cst) = try Spmap.find sp !eval_table with Not_found -> begin - let v = - match constant_opt_value (Global.env ()) cst with - | None -> NotAnElimination - | Some c -> compute_consteval c - in + let v = constant_descend cst in eval_table := Spmap.add sp v !eval_table; v end -- cgit v1.2.3