diff options
-rw-r--r-- | interp/constrintern.ml | 7 | ||||
-rw-r--r-- | interp/implicit_quantifiers.ml | 4 | ||||
-rw-r--r-- | interp/implicit_quantifiers.mli | 2 | ||||
-rw-r--r-- | plugins/subtac/subtac_classes.ml | 4 | ||||
-rw-r--r-- | toplevel/classes.ml | 4 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 2 |
6 files changed, 12 insertions, 11 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c251ffb24..aa836ea11 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -697,8 +697,9 @@ let push_loc_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar (ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty = - let ty = - if t then ty else + let ids = match na with Anonymous -> ids | Name na -> Idset.add na ids in + let ty, ids' = + if t then ty, ids else Implicit_quantifiers.implicit_application ids Implicit_quantifiers.combine_params_freevar ty in @@ -715,7 +716,7 @@ let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar match ty with | CApp (_, (_, CRef (Ident (loc,id))), _) -> id | _ -> id_of_string "H" - in Implicit_quantifiers.make_fresh ids (Global.env ()) id + in Implicit_quantifiers.make_fresh ids' (Global.env ()) id in Name name | _ -> na in (push_loc_name_env ~fail_anonymous lvar env' loc na), (na,b',None,ty') :: List.rev bl diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 7b1a1ff4c..a55daff36 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -225,7 +225,7 @@ let implicit_application env ?(allow_partial=true) f ty = with Not_found -> None in match is_class with - | None -> ty + | None -> ty, env | Some ((loc, id, par), gr) -> let avoid = Idset.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in let c, avoid = @@ -241,7 +241,7 @@ let implicit_application env ?(allow_partial=true) f ty = let pars = List.rev (List.combine ci rd) in let args, avoid = combine_params avoid f par pars in CAppExpl (loc, (None, id), args), avoid - in c + in c, avoid let implicits_of_rawterm l = let rec aux i c = diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 57eff0b86..0d28eccad 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -51,4 +51,4 @@ val combine_params_freevar : val implicit_application : Idset.t -> ?allow_partial:bool -> (Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) -> Topconstr.constr_expr * Names.Idset.t) -> - constr_expr -> constr_expr + constr_expr -> constr_expr * Idset.t diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index 6fe14da34..93b65cd00 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -95,7 +95,7 @@ let substitution_of_constrs ctx cstrs = let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) pri = let env = Global.env() in let isevars = ref Evd.empty in - let tclass = + let tclass, _ = match bk with | Implicit -> Implicit_quantifiers.implicit_application Idset.empty (* need no avoid *) @@ -110,7 +110,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p in t, avoid | None -> failwith ("new instance: under-applied typeclass")) cl - | Explicit -> cl + | Explicit -> cl, Idset.empty in let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in let k, ctx', imps, subst = diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 5633b7273..c5b54df33 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -127,7 +127,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri = let env = Global.env() in let evars = ref Evd.empty in - let tclass = + let tclass, ids = match bk with | Implicit -> Implicit_quantifiers.implicit_application Idset.empty ~allow_partial:false @@ -138,7 +138,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) t, avoid | None -> failwith ("new instance: under-applied typeclass")) cl - | Explicit -> cl + | Explicit -> cl, Idset.empty in let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in let k, ctx', len, imps, subst = diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index e02079fad..664b05f1d 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -163,7 +163,7 @@ let make_cases s = let show_match id = try let s = string_of_id (snd id) in - let patterns = make_cases s in + let patterns = List.rev (make_cases s) in let cases = List.fold_left (fun acc x -> |