diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 11 | ||||
| -rw-r--r-- | interp/constrintern.ml | 3 |
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 |