diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index afc8d3b70d..33df4ca978 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -121,7 +121,7 @@ let clenv_environments evd bound t = let mk_clenv_from_env environ sigma n (c,cty) = let evd = create_goal_evar_defs sigma in let (evd,args,concl) = clenv_environments evd n cty in - { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args)); + { templval = mk_freelisted (applist (c,args)); templtyp = mk_freelisted concl; evd = evd; env = environ } |