diff options
author | 2000-10-04 15:57:52 +0000 | |
---|---|---|
committer | 2000-10-04 15:57:52 +0000 | |
commit | db9beee355f93cc6403d1837dc9674d20ebce30e (patch) | |
tree | 2c26b6f27911489ccd026f3bad4a246feac9225f | |
parent | a5529d6bdf015aef6b67aab8dd392075e721290b (diff) |
Nouvelle stratégie de nommage dans Simpl pour Fix
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@653 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | pretyping/tacred.ml | 19 |
1 files 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 |