diff options
| author | herbelin | 2000-01-20 23:19:37 +0000 |
|---|---|---|
| committer | herbelin | 2000-01-20 23:19:37 +0000 |
| commit | 6f5043cf05c8c4e7ae9acc878dbb63d76bc805a7 (patch) | |
| tree | 43b3bc8324c5dfc8bef10bc0764128ce2b998fdf /library | |
| parent | 4689ba338247d4753a4cd873eb16ff3f1bd201d8 (diff) | |
Broutilles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@278 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/redinfo.ml | 14 | ||||
| -rw-r--r-- | library/redinfo.mli | 3 |
2 files changed, 8 insertions, 9 deletions
diff --git a/library/redinfo.ml b/library/redinfo.ml index f289273ece..0ea9cdd92b 100644 --- a/library/redinfo.ml +++ b/library/redinfo.ml @@ -9,7 +9,8 @@ open Constant open Reduction type constant_evaluation = - | Elimination of (int * constr) list * int * bool + | EliminationFix of (int * constr) list * int + | EliminationCases of int | NotAnElimination let eval_table = ref Spmap.empty @@ -45,20 +46,17 @@ let compute_consteval c = raise Elimconst) l in if list_distinct (List.map fst li) then - (li,n,true) + EliminationFix (li,n) else raise Elimconst | (DOPN(MutCase _,_) as mc,lapp) -> (match destCase mc with - | (_,_,Rel _,_) -> ([],n,false) + | (_,_,Rel _,_) -> EliminationCases n | _ -> raise Elimconst) | _ -> raise Elimconst in - try - let (lv,n,b) = srec 0 [] c in - Elimination (lv,n,b) - with Elimconst -> - NotAnElimination + try srec 0 [] c + with Elimconst -> NotAnElimination let constant_eval sp = try diff --git a/library/redinfo.mli b/library/redinfo.mli index 3f71baa982..1b600e57b3 100644 --- a/library/redinfo.mli +++ b/library/redinfo.mli @@ -12,7 +12,8 @@ open Term (section~\refsec{tacred}). *) type constant_evaluation = - | Elimination of (int * constr) list * int * bool + | EliminationFix of (int * constr) list * int + | EliminationCases of int | NotAnElimination val constant_eval : section_path -> constant_evaluation |