diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 3 | ||||
| -rw-r--r-- | interp/impargs.ml | 30 |
2 files changed, 11 insertions, 22 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6d4ab8b4d6..1d3b1bbb24 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1724,8 +1724,7 @@ let drop_notations_pattern looked_for genv = the domains of lambdas in the encoding of match in constr. This check is here and not in the parser because it would require duplicating the levels of the [pattern] rule. *) - CErrors.user_err ?loc ~hdr:"drop_notations_pattern" - (Pp.strbrk "Casts are not supported in this pattern.") + CErrors.user_err ?loc (Pp.strbrk "Casts are not supported in this pattern.") and in_pat_sc scopes x = in_pat false (x,snd scopes) and in_not top loc scopes (subst,substlist as fullsubst) args = function | NVar id -> diff --git a/interp/impargs.ml b/interp/impargs.ml index db102470b0..48961c6c8a 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -20,7 +20,6 @@ open Lib open Libobject open EConstr open Reductionops -open Namegen open Constrexpr module NamedDecl = Context.Named.Declaration @@ -247,24 +246,15 @@ let is_rigid env sigma t = is_rigid_head sigma t | _ -> true -let find_displayed_name_in sigma all avoid na (env, b) = - let envnames_b = (env, b) in - let flag = RenamingElsewhereFor envnames_b in - if all then compute_and_force_displayed_name_in sigma flag avoid na b - else compute_displayed_name_in sigma flag avoid na b - -let compute_implicits_names_gen all env sigma t = +let compute_implicits_names env sigma t = let open Context.Rel.Declaration in - let rec aux env avoid names t = + let rec aux env names t = let t = whd_all env sigma t in match kind sigma t with | Prod (na,a,b) -> - let na',avoid' = find_displayed_name_in sigma all avoid na.Context.binder_name (names,b) in - aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b + aux (push_rel (LocalAssum (na,a)) env) (na.Context.binder_name::names) b | _ -> List.rev names - in aux env Id.Set.empty [] t - -let compute_implicits_names = compute_implicits_names_gen true + in aux env [] t let compute_implicits_explanation_gen strict strongly_strict revpat contextual env sigma t = let open Context.Rel.Declaration in @@ -291,9 +281,9 @@ let compute_implicits_explanation_flags env sigma f t = (f.strict || f.strongly_strict) f.strongly_strict f.reversible_pattern f.contextual env sigma t -let compute_implicits_flags env sigma f all t = +let compute_implicits_flags env sigma f t = List.combine - (compute_implicits_names_gen all env sigma t) + (compute_implicits_names env sigma t) (compute_implicits_explanation_flags env sigma f t) let compute_auto_implicits env sigma flags enriching t = @@ -361,10 +351,10 @@ let positions_of_implicits (_,impls) = let rec prepare_implicits i f = function | [] -> [] - | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.") - | (Name id, Some imp)::imps -> + | (na, Some imp)::imps -> let imps' = prepare_implicits (i+1) f imps in - Some (ExplByName id,imp,(set_maximality Silent (Name id) i imps' f.maximal,true)) :: imps' + let expl = match na with Name id -> ExplByName id | Anonymous -> ExplByPos (i,None) in + Some (expl,imp,(set_maximality Silent na i imps' f.maximal,true)) :: imps' | _::imps -> None :: prepare_implicits (i+1) f imps let set_manual_implicits silent flags enriching autoimps l = @@ -393,7 +383,7 @@ let set_manual_implicits silent flags enriching autoimps l = let compute_semi_auto_implicits env sigma f t = if not f.auto then [DefaultImpArgs, []] - else let l = compute_implicits_flags env sigma f false t in + else let l = compute_implicits_flags env sigma f t in [DefaultImpArgs, prepare_implicits 1 f l] (*s Constants. *) |