diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 54 |
1 files changed, 24 insertions, 30 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index cc5d189e04..9cdcb9e38b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -462,15 +462,6 @@ let is_needed_for_correct_partial_application tail imp = exception Expl -let params_implicit n impl = - let rec aux n impl = - if n == 0 then true - else match impl with - | [] -> false - | imp :: impl when is_status_implicit imp -> aux (pred n) impl - | _ -> false - in aux n impl - (* Implicit args indexes are in ascending order *) (* inctx is useful only if there is a last argument to be deduced from ctxt *) let explicitize loc inctx impl (cf,f) args = @@ -689,7 +680,7 @@ let rec extern inctx scopes vars r = | head :: tail -> ip q locs' tail ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc) in - CRecord (loc, None, List.rev (ip projs locals args [])) + CRecord (loc, List.rev (ip projs locals args [])) with | Not_found | No_match | Exit -> extern_app loc inctx @@ -721,26 +712,29 @@ let rec extern inctx scopes vars r = (cases_predicate_names tml) vars in let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in let tml = List.map (fun (tm,(na,x)) -> - let na' = match na,tm with - | Anonymous, GVar (_, id) -> - begin match rtntypopt with - | None -> None - | Some ntn -> - if occur_glob_constr id ntn then - Some (Loc.ghost, Anonymous) - else None - end - | Anonymous, _ -> None - | Name id, GVar (_,id') when Id.equal id id' -> None - | Name _, _ -> Some (Loc.ghost,na) in - (sub_extern false scopes vars tm, - (na',Option.map (fun (loc,ind,nal) -> - let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in - let fullargs = - if !Flags.in_debugger then args else - Notation_ops.add_patterns_for_params ind args in - extern_ind_pattern_in_scope scopes vars ind fullargs - ) x))) tml in + let na' = match na,tm with + | Anonymous, GVar (_, id) -> + begin match rtntypopt with + | None -> None + | Some ntn -> + if occur_glob_constr id ntn then + Some (Loc.ghost, Anonymous) + else None + end + | Anonymous, _ -> None + | Name id, GVar (_,id') when Id.equal id id' -> None + | Name _, _ -> Some (Loc.ghost,na) in + (sub_extern false scopes vars tm, + na', + Option.map (fun (loc,ind,nal) -> + let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in + let fullargs = + if !Flags.in_debugger then args else + Notation_ops.add_patterns_for_params ind args in + extern_ind_pattern_in_scope scopes vars ind fullargs + ) x)) + tml + in let eqns = List.map (extern_eqn inctx scopes vars) eqns in CCases (loc,sty,rtntypopt',tml,eqns) |