aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/instances.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/instances.ml')
-rw-r--r--plugins/firstorder/instances.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 4c6355f61..04bca584f 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -77,7 +77,7 @@ let match_one_quantified_hyp sigma setref seq lf=
Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))->
if do_sequent sigma setref triv lf.id seq i dom lf.atoms then
setref:=IS.add ((Phantom dom),lf.id) !setref
- | _ -> anomaly (Pp.str "can't happen")
+ | _ -> anomaly (Pp.str "can't happen.")
let give_instances sigma lf seq=
let setref=ref IS.empty in