diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/correctness/ptactic.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/centaur.ml | 2 | ||||
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 3 |
3 files changed, 3 insertions, 4 deletions
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index a4b62c53c4..66633277a9 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -220,7 +220,7 @@ let correctness s p opttac = let env = Global.env () in let sign = Global.named_context () in let sigma = Evd.empty in - let cty = Reduction.nf_betaiota env sigma cty in + let cty = Reduction.nf_betaiota cty in let id = id_of_string s in start_proof id Declare.NeverDischarge sign cty; Penv.new_edited id (v,p); diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml index f48f04e7c3..6e1555d591 100644 --- a/contrib/interface/centaur.ml +++ b/contrib/interface/centaur.ml @@ -289,7 +289,7 @@ let ct_print_eval ast red_fun env evd judg = let {uj_val=value; uj_type=typ} = judg in let nvalue = red_fun value (* // Attention , ici il faut peut être utiliser des environnemenst locaux *) -and ntyp = nf_betaiota env evd typ in +and ntyp = nf_betaiota typ in (ctf_SearchResults !global_request_id, Some (P_pl (CT_premises_list diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 5f23c1d641..95a93cde73 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -265,8 +265,7 @@ let print_term inner_types l env csr = let inner_type_display env term = let type_of_term = - Reduction.nf_betaiota env (Evd.empty) - (R.get_type_of env (Evd.empty) term) + Reduction.nf_betaiota (R.get_type_of env (Evd.empty) term) in match R.get_sort_of env (Evd.empty) type_of_term with T.Prop T.Null -> InnerProp type_of_term |