diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-28 20:22:43 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-28 20:22:43 +0000 |
commit | 6bd55e5c17463d3868becba4064dba46c95c4028 (patch) | |
tree | d9883d5846ada3e5f0d049d711da7a1414f410ad /pretyping/pretyping.ml | |
parent | 5bb2935198434eceea41e1b966b56a175def396d (diff) |
- Second pass on implementation of let pattern. Parse "let ' par [as x]?
[in I] := t [return pred] in b", just as SSReflect does with let:.
Change implementation: no longer a separate AST node, just add a case_style
annotation on Cases to indicate it (if ML was dependently typed we
could ensure that LetPatternStyle Cases have only one term to be
matched and one branch, alas...). This factors out most code and we lose
no functionality (win ! win !). Add LetPat.v test suite.
- Slight improvement of inference of return clauses for dependent
pattern matching. If matching a variable of non-dependent type
under a tycon that mentions it while giving no return clause, the
dependency will be automatically infered. Examples at the end of
DepPat. Should get rid of most explicit returns under tycons.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10727 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretyping.ml')
-rw-r--r-- | pretyping/pretyping.ml | 18 |
1 files changed, 2 insertions, 16 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f9fcdb7b6..83381710d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -582,23 +582,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in { uj_val = v; uj_type = p } - - | RLetPattern (loc, c, p) -> - (* Just use cases typing *) - let j = - pretype tycon env evdref lvar - (RCases (loc, None, [c], [p])) - in - (* Change case info *) - let j' = match kind_of_term j.uj_val with - Case (ci, po, c, br) -> - let pp_info = { ci.ci_pp_info with style = LetPatternStyle } in - { j with uj_val = mkCase ({ ci with ci_pp_info = pp_info }, po, c, br) } - | _ -> j - in j' - | RCases (loc,po,tml,eqns) -> - Cases.compile_cases loc + | RCases (loc,sty,po,tml,eqns) -> + Cases.compile_cases loc sty ((fun vtyc env -> pretype vtyc env evdref lvar),evdref) tycon env (* loc *) (po,tml,eqns) |