diff options
| -rw-r--r-- | proofs/clenv.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index edda6de8b5..3555a386a5 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -367,7 +367,10 @@ let clenv_environments bound c = let mk_clenv_from wc (c,cty) = let (namenv,env,args,concl) = clenv_environments (-1) cty in - { templval = mk_freelisted (DOPN(AppL,Array.of_list (c::args))); + { templval = + mk_freelisted (match args with + | [] -> c + | _ -> DOPN(AppL,Array.of_list (c::args))); templtyp = mk_freelisted concl; namenv = namenv; env = env; |