summaryrefslogtreecommitdiff
path: root/interp/topconstr.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
commit86535d84cc3cffeee1dcd8545343f234e7285530 (patch)
tree9b221c283c2971f7ac151397231059e1d239e723 /interp/topconstr.ml
parent39efc41237ec906226a3a53d7396d51173495204 (diff)
parent61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff)
Diffstat (limited to 'interp/topconstr.ml')
-rw-r--r--interp/topconstr.ml15
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