diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-06-04 12:23:14 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:23:14 +0200 |
| commit | 86535d84cc3cffeee1dcd8545343f234e7285530 (patch) | |
| tree | 9b221c283c2971f7ac151397231059e1d239e723 /interp/topconstr.ml | |
| parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) | |
| parent | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff) | |
Remove non-DFSG contentsupstream/8.4_gamma0+really8.4beta2+dfsg
Diffstat (limited to 'interp/topconstr.ml')
| -rw-r--r-- | interp/topconstr.ml | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index b484d175..04d39fbf 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -239,7 +239,7 @@ let compare_recursive_parts found f (iterator,subc) = | GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term) | GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) -> (* We found a binding position where it differs *) - check_is_hole y t_x; + check_is_hole x t_x; check_is_hole y t_y; !diff = None && (diff := Some (x,y,None); aux c term) | _ -> @@ -564,8 +564,11 @@ let match_opt f sigma t1 t2 = match (t1,t2) with | _ -> raise No_match let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with - | (Name id1,Name id2) when List.mem id2 (fst metas) -> - alp, bind_env alp sigma id2 (GVar (dummy_loc,id1)) + | (_,Name id2) when List.mem id2 (fst metas) -> + let rhs = match na1 with + | Name id1 -> GVar (dummy_loc,id1) + | Anonymous -> GHole (dummy_loc,Evd.InternalHole) in + alp, bind_env alp sigma id2 rhs | (Name id1,Name id2) -> (id1,id2)::alp,sigma | (Anonymous,Anonymous) -> alp,sigma | _ -> raise No_match @@ -922,6 +925,12 @@ let names_of_local_binders bl = List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl) (**********************************************************************) +(* Miscellaneous *) + +let error_invalid_pattern_notation loc = + user_err_loc (loc,"",str "Invalid notation for pattern.") + +(**********************************************************************) (* Functions on constr_expr *) let constr_loc = function |