diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-09 10:35:30 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-09 10:35:30 +0000 |
| commit | d434ab34709e0ce40f049d709332800d9a96bcc5 (patch) | |
| tree | adc6e5ac006c3de8d9dbda1ad06905da31a5efdb /toplevel/command.ml | |
| parent | fa2571f711bf6ba6b99a04bf2cc10b68b37682f9 (diff) | |
Réorganisation de Impargs + mise en place d'une infrastructure
(notatemment des tables de parsing et d'affichage différenciées)
permettant au traducteur de changer les implicites
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3874 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 63c7cce93..6c33b3783 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -208,7 +208,7 @@ let interp_mutual lparams lnamearconstrs finite = let env' = Termops.push_rel_assum (Name recname,fullarity) env in let impls = if Impargs.is_implicit_args() - then Impargs.compute_implicits env_params fullarity + then Impargs.compute_implicits false env_params fullarity else [] in (env', (recname,impls)::ind_impls, (arity::arl))) (env0, [], []) lnamearconstrs |