diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-06 17:10:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-06 17:10:38 +0000 |
| commit | 48e922f2af1927b84801ea3781ba0acb30c0dd7f (patch) | |
| tree | 45dc2c10c7c5beed25dc4f7296534c342f95d05c /toplevel/minicoq.ml | |
| parent | 48af8fc25bdad1b8c2f475db67ff574e2311d641 (diff) | |
Canonisation de certains noms dans Pretyping, Asterm et Safe_typing
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@586 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/minicoq.ml')
| -rw-r--r-- | toplevel/minicoq.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index 5df900c26..945ff63ef 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -44,7 +44,7 @@ let rec globalize bv = function let check c = let c = globalize [] c in - let (j,u) = safe_machine !env c in + let (j,u) = safe_infer !env c in let ty = j_type j in let pty = pr_term CCI (env_of_safe_env !env) ty in mSGNL (hOV 0 [< 'sTR" :"; 'sPC; hOV 0 pty; 'fNL >]) |