diff options
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 4 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 1 |
2 files changed, 4 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 6497b6ff98..efd65ade15 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -122,6 +122,7 @@ let add_genarg tag pr = (** Constructors for cast type *) let dC t = CastConv t + (** Constructors for constr_expr *) let isCVar = function { CAst.v = CRef (qid,_) } -> qualid_is_ident qid | _ -> false let destCVar = function @@ -139,6 +140,7 @@ let mkCLambda ?loc name ty t = CAst.make ?loc @@ let mkCLetIn ?loc name bo t = CAst.make ?loc @@ CLetIn ((CAst.make ?loc name), bo, None, t) let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty) + (** Constructors for rawconstr *) let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None) let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) @@ -925,7 +927,7 @@ let of_ftactic ftac gl = let tac = Proofview.V82.of_tactic tac in let { sigma = sigma } = tac gl in let ans = match !r with - | None -> assert false (** If the tactic failed we should not reach this point *) + | None -> assert false (* If the tactic failed we should not reach this point *) | Some ans -> ans in (sigma, ans) diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 8672c55767..f0bb6f58a6 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -194,6 +194,7 @@ val cpattern_of_term : char * glob_constr_and_expr -> Geninterp.interp_sign -> c (** [do_once r f] calls [f] and updates the ref only once *) val do_once : 'a option ref -> (unit -> 'a) -> unit + (** [assert_done r] return the content of r. @raise Anomaly is r is [None] *) val assert_done : 'a option ref -> 'a |