diff options
| author | Maxime Dénès | 2018-07-26 11:47:33 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-07-26 11:47:33 +0200 |
| commit | 09c76adaff7adaada1c49479dfa9a4d0a4b416af (patch) | |
| tree | c59ff9f4ff5ca8c31f746b5d47618fd70085e621 /plugins | |
| parent | 3f2979c5f0fc289f41cc0e36b9914b3c8f7f77c5 (diff) | |
| parent | b9ff36b39eb193757ce57a89afe138cd09e759d7 (diff) | |
Merge PR #8050: Cleanup VERNAC EXTEND
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tacentries.ml | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 4b834d66d3..636cb8ebf8 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -594,15 +594,6 @@ let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol let clause_of_ty_ml = function | TyML (t,_) -> clause_of_sign t -let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function - | TUentry a -> ExtraArg a - | TUentryl (a,l) -> ExtraArg a - | TUopt(o) -> OptArg (prj o) - | TUlist1 l -> ListArg (prj l) - | TUlist1sep (l,_) -> ListArg (prj l) - | TUlist0 l -> ListArg (prj l) - | TUlist0sep (l,_) -> ListArg (prj l) - let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = fun sign tac -> match sign with @@ -617,7 +608,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i begin fun tac vals ist -> match vals with | [] -> assert false | v :: vals -> - let v' = Taccoerce.Value.cast (topwit (prj a)) v in + let v' = Taccoerce.Value.cast (topwit (Egramml.proj_symbol a)) v in f (tac v') vals ist end tac | TyAnonArg (a, sig') -> eval_sign sig' tac |