diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/centaur.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |