aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface
diff options
context:
space:
mode:
authorbarras2001-05-23 15:13:07 +0000
committerbarras2001-05-23 15:13:07 +0000
commitdc2e676c9cdedea43805c21a4b3203832a985f95 (patch)
tree849760ef13d1460d603ce9436c244922e13a6080 /contrib/interface
parenta023ff2e48aaf7ebfb15e10dc7cdb80ab2991e8e (diff)
amelioration des messages d'erreurs vis a vis des evars
ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
-rw-r--r--contrib/interface/centaur.ml2
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