diff options
| author | herbelin | 2000-09-10 20:37:37 +0000 |
|---|---|---|
| committer | herbelin | 2000-09-10 20:37:37 +0000 |
| commit | e72024e2292a50684b7f280d6efb8fee090e2dbf (patch) | |
| tree | fdba2d8c55f0c74aee8800a0e8c9aec3d3b8a584 /pretyping/cases.ml | |
| parent | 583992b6ce38655855f6625a26046ce84c53cdc1 (diff) | |
Suppression de Abst
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b01b3e283a..54869505ee 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -79,7 +79,7 @@ let make_case_ml isrec pred c ci lf = if isrec then DOPN(XTRA("REC"),Array.append [|pred;c|] lf) else - mkMutCaseA ci pred c lf + mkMutCase (ci, pred, c, lf) (* if arity of mispec is (p_bar:P_bar)(a_bar:A_bar)s where p_bar are the * K parameters. Then then build_notdep builds the predicate @@ -598,7 +598,7 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) = let predpred = lam_it (mkSort s) sign in let caseinfo = make_default_case_info mis in let brs = array_map2 abstract_conclusion typs cstrs in - let predbody = mkMutCaseA caseinfo predpred (Rel 1) brs in + let predbody = mkMutCase (caseinfo, predpred, Rel 1, brs) in let pred = lam_it (lift (List.length sign) typn) sign in failwith "TODO4-2"; (true,pred) @@ -833,7 +833,7 @@ and match_current pb (n,tm) = find_predicate pb.env pb.isevars pb.pred brtyps cstrs current indt in let ci = make_case_info mis None tags in - { uj_val = mkMutCaseA ci (*eta_reduce_if_rel*) pred current brvals; + { uj_val = mkMutCase (ci, (*eta_reduce_if_rel*)pred,current,brvals); uj_type = make_typed typ s } and compile_further pb firstnext rest = |