summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/extraction/extraction.ml6
-rw-r--r--contrib/firstorder/unify.ml6
-rw-r--r--contrib/funind/functional_principles_proofs.ml16
-rw-r--r--contrib/interface/showproof.ml2
-rw-r--r--contrib/subtac/subtac_cases.ml11
-rw-r--r--contrib/subtac/subtac_obligations.ml2
-rw-r--r--contrib/xml/cic2acic.ml6
-rw-r--r--contrib/xml/doubleTypeInference.ml8
8 files changed, 30 insertions, 27 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index fa006c1c..2cf457c6 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extraction.ml 11459 2008-10-16 16:29:07Z letouzey $ i*)
+(*i $Id: extraction.ml 11897 2009-02-09 19:28:02Z barras $ i*)
(*i*)
open Util
@@ -177,7 +177,7 @@ let parse_ind_args si args relmax =
let rec extract_type env db j c args =
- match kind_of_term (whd_betaiotazeta c) with
+ match kind_of_term (whd_betaiotazeta Evd.empty c) with
| App (d, args') ->
(* We just accumulate the arguments. *)
extract_type env db j d (Array.to_list args' @ args)
@@ -285,7 +285,7 @@ and extract_type_app env db (r,s) args =
and extract_type_scheme env db c p =
if p=0 then extract_type env db 0 c []
else
- let c = whd_betaiotazeta c in
+ let c = whd_betaiotazeta Evd.empty c in
match kind_of_term c with
| Lambda (n,t,d) ->
extract_type_scheme (push_rel_assum (n,t) env) db d (p-1)
diff --git a/contrib/firstorder/unify.ml b/contrib/firstorder/unify.ml
index 1dd13cbe..27c06f54 100644
--- a/contrib/firstorder/unify.ml
+++ b/contrib/firstorder/unify.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: unify.ml 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: unify.ml 11897 2009-02-09 19:28:02Z barras $ i*)
open Util
open Formula
@@ -42,8 +42,8 @@ let unif t1 t2=
Queue.add (t1,t2) bige;
try while true do
let t1,t2=Queue.take bige in
- let nt1=head_reduce (whd_betaiotazeta t1)
- and nt2=head_reduce (whd_betaiotazeta t2) in
+ let nt1=head_reduce (whd_betaiotazeta Evd.empty t1)
+ and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in
match (kind_of_term nt1),(kind_of_term nt2) with
Meta i,Meta j->
if i<>j then
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 9f3e412a..b13bea9d 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -252,7 +252,8 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type =
(new_end_of_type,0,witness_fun)
context
in
- let new_type_of_hyp = Reductionops.nf_betaiota new_type_of_hyp in
+ let new_type_of_hyp =
+ Reductionops.nf_betaiota Evd.empty new_type_of_hyp in
let new_ctxt,new_end_of_type =
Sign.decompose_prod_n_assum ctxt_size new_type_of_hyp
in
@@ -708,7 +709,8 @@ let build_proof
| Const _ ->
do_finalize dyn_infos g
| Lambda _ ->
- let new_term = Reductionops.nf_beta dyn_infos.info in
+ let new_term =
+ Reductionops.nf_beta Evd.empty dyn_infos.info in
build_proof do_finalize {dyn_infos with info = new_term}
g
| LetIn _ ->
@@ -1056,7 +1058,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
let bodies_with_all_params =
Array.map
(fun body ->
- Reductionops.nf_betaiota
+ Reductionops.nf_betaiota Evd.empty
(applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
List.rev_map var_of_decl princ_params))
)
@@ -1093,12 +1095,12 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
let body_with_param,num =
let body = get_body fnames.(i) in
let body_with_full_params =
- Reductionops.nf_betaiota (
+ Reductionops.nf_betaiota Evd.empty (
applist(body,List.rev_map var_of_decl full_params))
in
match kind_of_term body_with_full_params with
| Fix((_,num),(_,_,bs)) ->
- Reductionops.nf_betaiota
+ Reductionops.nf_betaiota Evd.empty
(
(applist
(substl
@@ -1174,7 +1176,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
nb_rec_hyps = -100;
rec_hyps = [];
info =
- Reductionops.nf_betaiota
+ Reductionops.nf_betaiota Evd.empty
(applist(fix_body,List.rev_map mkVar args_id));
eq_hyps = []
}
@@ -1236,7 +1238,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
nb_rec_hyps = -100;
rec_hyps = [];
info =
- Reductionops.nf_betaiota
+ Reductionops.nf_betaiota Evd.empty
(applist(fbody_with_full_params,
(List.rev_map var_of_decl princ_params)@
(List.rev_map mkVar args_id)
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index cf861642..2ab62763 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1361,7 +1361,7 @@ and natural_cutintro ig lh g gs arg ltree =
{ihsg=No_subgoals_hyp;isgintro=""}
(List.nth ltree 0))]
]
-and whd_betadeltaiota x = whd_betaiotaevar (Global.env()) Evd.empty x
+and whd_betadeltaiota x = whd_betaiota Evd.empty x
and type_of_ast s c = type_of (Global.env()) Evd.empty (constr_of_ast c)
and prod_head t =
match (kind_of_term (strip_outer_cast t)) with
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 094226ff..1d213db9 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_cases.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: subtac_cases.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Cases
open Util
@@ -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 cc1e2dde..d2e831ef 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -282,7 +282,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' =
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index c62db00b..13e5e6d5 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -245,9 +245,9 @@ let typeur sigma metamap =
let Inductiveops.IndType(_,realargs) =
try Inductiveops.find_rectype env sigma (type_of env c)
with Not_found -> Util.anomaly "type_of: Bad recursive type" in
- let t = Reductionops.whd_beta (T.applist (p, realargs)) in
+ let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in
(match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with
- | T.Prod _ -> Reductionops.whd_beta (T.applist (t, [c]))
+ | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c]))
| _ -> t)
| T.Lambda (name,c1,c2) ->
T.mkProd (name, c1, type_of (Environ.push_rel (name,None,c1) env) c2)
@@ -390,7 +390,7 @@ Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-ty
(* We need to refresh the universes because we are doing *)
(* type inference on an already inferred type. *)
{D.synthesized =
- Reductionops.nf_beta
+ Reductionops.nf_beta evar_map
(CPropRetyping.get_type_of env evar_map
(Termops.refresh_universes tt)) ;
D.expected = None}
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index de8c540c..17d1d5da 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -163,7 +163,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
| hj::restjl ->
match T.kind_of_term (Reduction.whd_betadeltaiota env typ) with
T.Prod (_,c1,c2) ->
- (Some (Reductionops.nf_beta c1)) ::
+ (Some (Reductionops.nf_beta sigma c1)) ::
(aux (T.subst1 hj c2) restjl)
| _ -> assert false
in
@@ -183,7 +183,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
| Some ety ->
match T.kind_of_term (Reduction.whd_betadeltaiota env ety) with
T.Prod (_,_,expected_target_type) ->
- Some (Reductionops.nf_beta expected_target_type)
+ Some (Reductionops.nf_beta sigma expected_target_type)
| _ -> assert false
in
let j' = execute env1 sigma c2 expectedc2type in
@@ -214,14 +214,14 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
Typeops.judge_of_letin env name j1 j2 j3
| T.Cast (c,k,t) ->
- let cj = execute env sigma c (Some (Reductionops.nf_beta t)) in
+ let cj = execute env sigma c (Some (Reductionops.nf_beta sigma t)) in
let tj = execute env sigma t None in
let tj = type_judgment env sigma tj in
let j, _ = Typeops.judge_of_cast env cj k tj in
j
in
let synthesized = E.j_type judgement in
- let synthesized' = Reductionops.nf_beta synthesized in
+ let synthesized' = Reductionops.nf_beta sigma synthesized in
let types,res =
match expectedty with
None ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 22:28:39 +0000