diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-07 15:08:12 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-07 15:08:12 +0000 |
| commit | 26ca22424b286f5ff22a1fa97c38d15e224b3dc2 (patch) | |
| tree | 190e12acf505e47d3a81ef0fd625a405ff782c04 /pretyping/clenv.ml | |
| parent | 5f9b04da0f3c72f4b582cd094edae721b1bc9a9e (diff) | |
- Documentation of the Program tactics.
- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists.
Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop.
- Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/clenv.ml')
| -rw-r--r-- | pretyping/clenv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index cb8c2cf2b..d7c8a6dd0 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -31,7 +31,7 @@ open Mod_subst (* *) let w_coerce env c ctyp target evd = let j = make_judge c ctyp in - let (evd',j') = Coercion.Default.inh_conv_coerce_to dummy_loc env evd j target in + let (evd',j') = Coercion.Default.inh_conv_coerce_to dummy_loc env evd j (mk_tycon_type target) in (evd',j'.uj_val) let pf_env gls = Global.env_of_context gls.it.evar_hyps |