summaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml11
-rw-r--r--interp/constrintern.ml3
2 files changed, 9 insertions, 5 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 19e1fef5..20b9c2a3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -250,7 +250,9 @@ and check_same_fix_binder bl1 bl2 =
check_same_binder ([na1],default_binder_kind,def1) ([na2],default_binder_kind,def2)
| _ -> failwith "not same binder") bl1 bl2
-let is_same_type c d = try let () = check_same_type c d in true with Failure _ -> false
+let is_same_type c d =
+ try let () = check_same_type c d in true
+ with Failure _ | Invalid_argument _ -> false
(**********************************************************************)
(* mapping patterns to cases_pattern_expr *)
@@ -374,11 +376,12 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
| (keyrule,pat,n as _rule)::rules ->
try
match t,n with
- | PatCstr (loc,(ind,_),l,na), n when n = Some 0 or n = None or
- n = Some(fst(Global.lookup_inductive ind)).Declarations.mind_nparams ->
+ | PatCstr (loc,(ind,_),l,na), n when (n = Some 0 or n = None or
+ n = Some(fst(Global.lookup_inductive ind)).Declarations.mind_nparams)
+ && (match keyrule with SynDefRule _ -> true | _ -> false) ->
(* Abbreviation for the constructor name only *)
(match keyrule with
- | NotationRule (sc,ntn) -> raise No_match
+ | NotationRule _ -> assert false
| SynDefRule kn ->
let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
let l = List.map (extern_cases_pattern_in_scope allscopes vars) l in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 45df005c..81e4501a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1411,7 +1411,8 @@ let internalize sigma globalenv env allow_patvar lvar c =
| None ->
[], None in
let na = match tm', na with
- | GVar (loc,id), None when Idset.mem id env.ids -> loc,Name id
+ | GVar (loc,id), None when not (List.mem_assoc id (snd lvar)) ->
+ loc,Name id
| GRef (loc, VarRef id), None -> loc,Name id
| _, None -> dummy_loc,Anonymous
| _, Some (loc,na) -> loc,na in