diff options
| author | herbelin | 2000-09-10 07:51:27 +0000 |
|---|---|---|
| committer | herbelin | 2000-09-10 07:51:27 +0000 |
| commit | 583992b6ce38655855f6625a26046ce84c53cdc1 (patch) | |
| tree | 71e61d46a919e5dfb65c0e87cfb9ff6d4f337f47 | |
| parent | 79dc33cbc403ebab0bd1fe815c13f740f0a1b850 (diff) | |
Ajout d'un LetIn primitif.
Abstraction de constr via kind_of_constr dans une bonne partie du code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@592 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | library/redinfo.ml | 36 |
1 files changed, 19 insertions, 17 deletions
diff --git a/library/redinfo.ml b/library/redinfo.ml index bc51d5d75d..9e5c86a528 100644 --- a/library/redinfo.ml +++ b/library/redinfo.ml @@ -3,7 +3,7 @@ open Util open Names -open Generic +(*i open Generic i*) open Term open Declarations open Reduction @@ -30,29 +30,31 @@ exception Elimconst let compute_consteval c = let rec srec n labs c = - match whd_betadeltaeta_stack (Global.env()) Evd.empty c [] with - | (DOP2(Lambda, t, DLAM(_,g)), []) -> - srec (n+1) (t::labs) g - | (DOPN(Fix (nv,i), bodies), l) -> + let c',l = whd_betadeltaeta_stack (Global.env()) Evd.empty c [] in + match kind_of_term c' with + | IsLambda (_,t,g) when l=[] -> srec (n+1) (t::labs) g + | IsFix ((nv,i),(tys,_,bds)) -> if (List.length l) > n then raise Elimconst; + let nbfix = Array.length bds in let li = - List.map (function - | Rel k -> - if array_for_all (noccurn k) bodies then - (k, List.nth labs (k-1)) - else - raise Elimconst - | _ -> - raise Elimconst) l + List.map + (function + | Rel k -> + if + array_for_all (noccurn k) tys + && array_for_all (noccurn (k+nbfix)) bds + then + (k, List.nth labs (k-1)) + else + raise Elimconst + | _ -> + raise Elimconst) l in if list_distinct (List.map fst li) then EliminationFix (li,n) else raise Elimconst - | (DOPN(MutCase _,_) as mc,lapp) -> - (match destCase mc with - | (_,_,Rel _,_) -> EliminationCases n - | _ -> raise Elimconst) + | IsMutCase (_,_,Rel _,_) -> EliminationCases n | _ -> raise Elimconst in try srec 0 [] c |