diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-21 11:41:23 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-21 11:41:23 +0000 |
| commit | 7b908ce89ca8c4bc85a787e1e57bb64f1e102c00 (patch) | |
| tree | 0ddbeb4ecbae579a8eea1fcfede8a1dac316550d /pretyping | |
| parent | 4598007c8b8bfc7e591e53116e37f49743317fec (diff) | |
Inlining let-in (i.e. trace of aliases) in extract_predicate for what
seems to provide a better rendering in pattern-matching
compilation. Did it also in compile_generalization but not sure the
uj_typ is not dropped anyway.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14708 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index d764c908d..99fd7082f 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -851,7 +851,7 @@ let rec extract_predicate ccl = function (* substitution already done in build_branch *) extract_predicate ccl tms | Abstract (i,d)::tms -> - mkProd_or_LetIn d (extract_predicate ccl tms) + mkProd_wo_LetIn d (extract_predicate ccl tms) | Pushed ((cur,NotInd _),_,na)::tms -> let tms = if na<>Anonymous then lift_tomatch_stack 1 tms else tms in let pred = extract_predicate ccl tms in @@ -1300,7 +1300,7 @@ and compile_generalization pb i d rest = mat = List.map (push_generalized_decl_eqn pb.env i d) pb.mat } in let j = compile pb in { uj_val = mkLambda_or_LetIn d j.uj_val; - uj_type = mkProd_or_LetIn d j.uj_type } + uj_type = mkProd_wo_LetIn d j.uj_type } and compile_alias pb (orig,(_,ci,_ as alias),isdeppred) rest = let pb = |