diff options
| author | herbelin | 2000-09-12 11:02:30 +0000 |
|---|---|---|
| committer | herbelin | 2000-09-12 11:02:30 +0000 |
| commit | 6fcd224c128ae5e81f4cce9d5de1ac45883cfebf (patch) | |
| tree | 9d5c886b18ca44f3a24de7b58c7dd7ca8bc88eec /toplevel | |
| parent | 9248485d71d1c9c1796a22e526e07784493e2008 (diff) | |
Modification mkAppL; abstraction via kind_of_term; changement dans Reduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/discharge.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 9a55f5adfb..3240e9db51 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -204,7 +204,7 @@ let expmod_constr oldenv modlist c = | DOP2(Cast,c,t) -> (DOP2(Cast,f c,f t)) | c -> f c in - let c' = modify_opers expfun (fun a b -> mkAppL [|a; b|]) modlist c in + let c' = modify_opers expfun (fun a b -> mkAppL (a, [|b|])) modlist c in match c' with | DOP2 (Cast,val_0,typ) -> DOP2 (Cast,simpfun val_0,simpfun typ) | _ -> simpfun c' |