diff options
| author | jforest | 2006-04-24 07:59:57 +0000 |
|---|---|---|
| committer | jforest | 2006-04-24 07:59:57 +0000 |
| commit | 4d7dd37ecc7e3d0dcc58d15eca53972cf41be057 (patch) | |
| tree | 728ad922b97966a6cd715cefac0a621062b9fab9 /contrib/funind/rawtermops.ml | |
| parent | 2ff58aa2c8592a5ce56815e10c8477f481ab25fd (diff) | |
+ Handling "if" and cast in GenFixpoint
+ Correcting a bug in recursives funcitons detection in GenFixpoint
+ Parially handling applied binders in funcitonal principles generation tactic
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8725 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/funind/rawtermops.ml')
| -rw-r--r-- | contrib/funind/rawtermops.ml | 22 |
1 files changed, 19 insertions, 3 deletions
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml index 99bf2bf1d1..cd09fb5f29 100644 --- a/contrib/funind/rawtermops.ml +++ b/contrib/funind/rawtermops.ml @@ -123,7 +123,13 @@ let change_vars = List.map (fun (e,x) -> (change_vars mapping e,x)) el, List.map (change_vars_br mapping) brl ) - | RIf _ -> error "Not handled RIf" + | RIf(loc,b,(na,e_option),lhs,rhs) -> + RIf(loc, + change_vars mapping b, + (na,option_app (change_vars mapping) e_option), + change_vars mapping lhs, + change_vars mapping rhs + ) | RRec _ -> error "Not handled RRec" | RSort _ -> rt | RHole _ -> rt @@ -297,7 +303,12 @@ let rec alpha_rt excluded rt = List.map (function (rt,i) -> alpha_rt excluded rt, i) el in RCases(loc,infos,new_el,List.map (alpha_br excluded) brl) - | RIf _ -> error "Not handled RIf" + | RIf(loc,b,(na,e_o),lhs,rhs) -> + RIf(loc,alpha_rt excluded b, + (na,option_app (alpha_rt excluded) e_o), + alpha_rt excluded lhs, + alpha_rt excluded rhs + ) | RRec _ -> error "Not handled RRec" | RSort _ -> rt | RHole _ -> rt @@ -449,7 +460,12 @@ let replace_var_by_term x_id term = List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el, List.map replace_var_by_pattern_br brl ) - | RIf _ -> raise (UserError("",str "Not handled RIf")) + | RIf(loc,b,(na,e_option),lhs,rhs) -> + RIf(loc, replace_var_by_pattern b, + (na,option_app replace_var_by_pattern e_option), + replace_var_by_pattern lhs, + replace_var_by_pattern rhs + ) | RRec _ -> raise (UserError("",str "Not handled RRec")) | RSort _ -> rt | RHole _ -> rt |