diff options
| author | barras | 2009-02-06 21:25:52 +0000 |
|---|---|---|
| committer | barras | 2009-02-06 21:25:52 +0000 |
| commit | 6160f53e89800a785d773c4130b08fbe7c345651 (patch) | |
| tree | 88b2aadfa1c697ca8686818be25fcf9449b5dba6 /contrib/subtac | |
| parent | 370575d3e98f375969983d26f62a1ddeab524d0e (diff) | |
pushed evar reduction in kernel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac')
| -rw-r--r-- | contrib/subtac/subtac_cases.ml | 9 | ||||
| -rw-r--r-- | contrib/subtac/subtac_obligations.ml | 2 |
2 files changed, 6 insertions, 5 deletions
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index 3e80be65ef..09ee456d7c 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -822,7 +822,7 @@ let infer_predicate loc env isevars typs cstrs indf = (* Empiric normalization: p may depend in a irrelevant way on args of the*) (* cstr as in [c:{_:Alpha & Beta}] match c with (existS a b)=>(a,b) end *) let typs = - Array.map (local_strong (whd_betaevar empty_env (Evd.evars_of !isevars))) typs + Array.map (local_strong whd_beta (Evd.evars_of !isevars)) typs in let eqns = array_map2 prepare_unif_pb typs cstrs in (* First strategy: no dependencies at all *) @@ -1042,9 +1042,10 @@ let find_predicate loc env isevars p typs cstrs current match p with | Some p -> abstract_predicate env (Evd.evars_of !isevars) indf current tms p | None -> infer_predicate loc env isevars typs cstrs indf in - let typ = whd_beta (applist (pred, realargs)) in + let typ = whd_beta (Evd.evars_of !isevars) (applist (pred, realargs)) in if dep then - (pred, whd_beta (applist (typ, [current])), new_Type ()) + (pred, whd_beta (Evd.evars_of !isevars) (applist (typ, [current])), + new_Type ()) else (pred, typ, new_Type ()) @@ -1246,7 +1247,7 @@ and match_current pb tomatch = find_predicate pb.caseloc pb.env pb.isevars pb.pred brtyps cstrs current indt pb.tomatch in let ci = make_case_info pb.env mind pb.casestyle in - let case = mkCase (ci,nf_betaiota pred,current,brvals) in + let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in let inst = List.map mkRel deps in { uj_val = applist (case, inst); uj_type = substl inst typ } diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index df700e1b1f..8b8bb9ab47 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -288,7 +288,7 @@ let declare_obligation obl body = print_message (Subtac_utils.definition_message obl.obl_name); { obl with obl_body = Some (mkConst constant) } -let red = Reductionops.nf_betaiota +let red = Reductionops.nf_betaiota Evd.empty let init_prog_info n b t deps fixkind notations obls impls kind hook = let obls' = |